Operation: unlink



Section Unlink.



Variable s: SFSstate.




Some preliminary definitions


Definition unlink_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 unlink_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) (unlink_oSC o) (unlink_acl o)
          (secmat s) (unlink_files o) (unlink_directories o)).




Operation definition


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

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



End Unlink.

Hints Unfold unlink_oSC unlink_acl.