Operation: oscstat
|
Require Export DACandMAC.
Section Oscstat.
Variable s: SFSstate.
Operation definition |
Inductive oscstat
[u:SUBJECT; o:OBJECT] : SFSstate -> (Exc SecClass) -> Prop :=
|OscstatOK:
(PreMAC s u o)
->(oscstat u o s (fOSC (objectSC s) o)).
|
|
End Oscstat.