Operation: sscstat

  • This operation outputs the security class of a given subject.
  • The security class of the invoking user should be less or equal than that of the requested user.

Require Export SFSstate.

Implicit Arguments On.



Section Sscstat.



Variable s: SFSstate.

Operation definition



Inductive sscstat
  [u,user:SUBJECT]: SFSstate -> (Exc SecClass) -> Prop :=

  |SscstatOK:
     Cases (fSSC (subjectSC s) user)
           (fSSC (subjectSC s) u) of
      |None _ => True
      |_ None => True
      |(Some y)
       (Some z) => (le_sc y z)
     end -> (sscstat u user s (fSSC (subjectSC s) user)).

End Sscstat.

Index
This page has been generated by coqdoc