Operation: aclstat

• This operation outputs the information stored in the ACL of a givenobject. PreDACRead should be satisfied for the invoking user andobject. There is no change of state.

Require Export DACandMAC.



Implicit Arguments On.



Section Aclstat.



Variable s:SFSstate.

Operation definition



Inductive aclstat
  [u:SUBJECT; o:OBJECT]: SFSstate -> (Exc AccessCtrlListData) -> Prop:=

  |AclstatOK:
     (PreDACRead s u o)
     ->(aclstat u o s (facl (acl s) o)).



End Aclstat.