Require Export DACandMAC.

Set Implicit Arguments.
Unset Strict Implicit.



Section Aclstat.

Variable s : SFSstate.

Inductive aclstat (u : SUBJECT) (o : OBJECT) :
SFSstate → Exc AccessCtrlListData → Prop :=
    AclstatOK :
      PreDACRead s u o →
      aclstat u o s
        match facl (acl s) o with
        | None ⇒ None (A:=AccessCtrlListData)
        | Some y ⇒
            Some
              (acldata (owner y) (group y) (UsersReaders y)
                 (GroupReaders y) (UsersWriters y)
                 (GroupWriters y) (UsersOwners y) (GroupOwners y))
        end.

End Aclstat.