Operation: rmdir

Require Export DACandMAC.



Section Rmdir.



Variable s: SFSstate.



Some preliminary definitions


Definition rmdir_oSC [o:OBJECT] : (set OBJECT*SecClass) :=
 Cases (fOSC (objectSC s) o) of
  |None => (objectSC s)
  |(Some y) => (set_remove OSCeq_dec (o,y) (objectSC s))
 end.



Definition rmdir_acl [o:OBJECT] : (set OBJECT*AccessCtrlListData) :=
 Cases (facl (acl s) o) of
  |None => (acl s)
  |(Some y) => (set_remove ACLeq_dec (o,y) (acl s))
 end.



Next state definition



Local t [o:OBJECT] : SFSstate :=
   (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
          (RootGrp s) (SecAdmGrp s) (rmdir_oSC o) (rmdir_acl o)
          (secmat s) (files s) (rmdir_directories o)).




Operation definition

Inductive rmdir [u:SUBJECT; o:OBJECT] : SFSstate -> Prop :=

  |RmdirOK:
     (ObjType o)=Directory
     ->(set_In (MyDir (ObjName o)) (domd (directories s)))
     ->Cases (fsecmat (secmat s) (MyDir (ObjName o))) of
        |None => False
        |(Some y) => (set_In u (ActWriters y))
       end
     ->~(set_In o (domsecmat (secmat s)))
     ->(rmdir u o (t o)).



End Rmdir.

Hints Unfold rmdir_oSC rmdir_acl.