Require ModelProperties.
User defined tactics |
Tactic Definition OpDontChangeStPSS
:=
Intros s t Sub SS TF;
Inversion TF;
Rewrite <- H3;
Auto.
Tactic Definition OpDontChangeStPSP :=
Intros s t Sub SP TF;
Inversion TF;
Rewrite <- H3;
Auto.
Tactic Definition StartPCP :=
Intros;
Unfold PreservesControlProp;
Intros Sub TF;
Inversion TF;
Unfold ControlProperty;
Right;
Left;
Split with o;
Intro MAC;
Inversion MAC.
Tactic Definition StartPSS :=
Intros s t Sub SS TF;
Inversion TF.
Tactic Definition BreakSS :=
Unfold SecureState in SS;
Elim SS;
Intros DAC MAC.
Tactic Definition StartPSP :=
Intros s t Sub SP TF;
Inversion TF.
Tactic Definition ProvePCP :=
Intros;
Unfold PreservesControlProp;
Intros Sub TF; Inversion TF;
Inversion H;
Unfold ControlProperty;
EAuto.
Lemmas |
Lemma ReadWriteImpRead:
(s:SFSstate)(DACSecureState s)
->(u:SUBJECT; o:OBJECT)
Cases (fsecmat (secmat s) o) of
|(Some y) => ((set_In u (ActReaders y))->(PreDACRead s u o))
| None => True
end.
Unfold DACSecureState.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) =>
((set_In u (ActReaders y))->(PreDACRead s u o))
/\((set_In u (ActWriters y))->(PreDACWrite s u o))
| None => True
end.
Elim (fsecmat (secmat s) o).
Intros.
Elim H0; Intros.
Auto.
Auto.
Apply H.
Qed.
|
|
Lemma ReadWriteImpWrite:
(s:SFSstate)(DACSecureState s)
->(u:SUBJECT; o:OBJECT)
Cases (fsecmat (secmat s) o) of
|(Some y) => ((set_In u (ActWriters y))->(PreDACWrite s u o))
| None => True
end.
Unfold DACSecureState.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) =>
((set_In u (ActReaders y))->(PreDACRead s u o))
/\((set_In u (ActWriters y))->(PreDACWrite s u o))
| None => True
end.
Elim (fsecmat (secmat s) o).
Intros.
Elim H0; Intros.
Auto.
Auto.
Apply H.
Qed.
|
|
Lemma TwoImpLeft:
(s:SFSstate; u:SUBJECT)
((rw:ReadersWriters)
(set_In rw (ransecmat (secmat s)))
->~(set_In u (ActReaders rw))/\~(set_In u (ActWriters rw)))
->((rw:ReadersWriters)
(set_In rw (ransecmat (secmat s)))
->~(set_In u (ActReaders rw))).
Intros.
Cut ~(set_In u (ActReaders rw))/\~(set_In u (ActWriters rw)).
Tauto.
Auto.
Qed.
|
|
Lemma TwoImpRight:
(s:SFSstate; u:SUBJECT)
((rw:ReadersWriters)
(set_In rw (ransecmat (secmat s)))
->~(set_In u (ActReaders rw))/\~(set_In u (ActWriters rw)))
->((rw:ReadersWriters)
(set_In rw (ransecmat (secmat s)))
->~(set_In u (ActWriters rw))).
Intros.
Cut ~(set_In u (ActReaders rw))/\~(set_In u (ActWriters rw)).
Tauto.
Auto.
Qed.
|
|
Lemma UniqNames:
(s:SFSstate; o:OBJECT)
(FuncPre1 s)
->~(set_In ((ObjName o),File) (domf (files s)))
->~(set_In ((ObjName o),Directory) (domd (directories s)))
->~(set_In o (DOM OBJeq_dec (acl s))).
Intro; Intro; Unfold FuncPre1; Elim o; Simpl; Intros.
Cut ((o:OBJECT)
(set_In o (DOM OBJeq_dec (directories s)))->(ObjType o)=Directory)
/\((o:OBJECT)(set_In o (DOM OBJeq_dec (files s)))->(ObjType o)=File)
/\(DOM OBJeq_dec (acl s))
=(set_union OBJeq_dec (DOM OBJeq_dec (files s))
(DOM OBJeq_dec (directories s))).
Intro CUT; Elim CUT; Intros.
Elim H3; Intros.
Rewrite H5; Intro.
Cut (set_In (a,File) (domf (files s)))
\/(set_In (a,Directory) (domd (directories s))).
Intro H7; Elim H7; Intro.
Auto.
Auto.
Generalize H6; Elim b; Intro.
Left; Cut ~(set_In (a,File) (DOM OBJeq_dec (directories s))).
Intro; Unfold domf.
Cut (set_In (a,File)
(set_union OBJeq_dec (DOM OBJeq_dec (directories s))
(DOM OBJeq_dec (files s)))).
Intro; EAuto.
Auto.
Intro; Absurd (ObjType (a,File))=Directory.
Simpl.
Intro H11; Discriminate H11.
Auto.
Auto.
Right.
Cut ~(set_In (a,Directory) (DOM OBJeq_dec (files s))).
Intro; Unfold domd; EAuto.
Intro; Absurd (ObjType (a,Directory))=File.
Simpl.
Intro H11; Discriminate H11.
Auto.
Auto.
Qed.
Hints Resolve UniqNames.
|
|
Lemma eq_scIMPLYle_sc: (a,b:SecClass)(eq_sc a b)->(le_sc a b).
Unfold eq_sc le_sc; Intros.
Elim H; Intros.
Rewrite H0; Rewrite H1.
Auto.
Qed.
|
|
Lemma NotInDOMIsUndef2:
(s:SFSstate; o1,o2:OBJECT)
~(set_In o1 (domsecmat (secmat s)))
->o1=o2
->(None ReadersWriters)=(fsecmat (secmat s) o2).
Intros.
Symmetry.
Rewrite H0 in H.
Unfold fsecmat; Apply NotInDOMIsUndef; Auto.
Qed.
|
|
Lemma NotInDOMIsUndef3:
(s:SFSstate; p:OBJNAME; o:OBJECT)
(FuncPre1 s)
->(FuncPre3 s)
->~(set_In (p,File) (domf (files s)))
->~(set_In (p,Directory) (domd (directories s)))
->p=(ObjName o)
->(None ReadersWriters)=(fsecmat (secmat s) o).
Intros until o; Elim o; Simpl.
Intros until b; Elim b; Intros.
Rewrite <- H3.
Symmetry; Unfold fsecmat; Apply NotInDOMIsUndef.
Cut ~(set_In (p,File) (DOM OBJeq_dec (acl s))).
Unfold FuncPre3 Included in H3.
Unfold FuncPre3 Included in H0.
Auto.
Apply UniqNames; Auto.
Rewrite <- H3.
Symmetry; Unfold fsecmat; Apply NotInDOMIsUndef.
Cut ~(set_In (p,Directory) (DOM OBJeq_dec (acl s))).
Unfold FuncPre3 Included in H3.
Unfold FuncPre3 Included in H0.
Auto.
Apply UniqNames; Auto.
Qed.
|
|
Lemma EqfOSC6:
(s:SFSstate; o1,o2:OBJECT; sc:SecClass)
~o1=o2
->(fOSC (objectSC s) o2)=(fOSC (chobjsc_SC s o1 sc) o2).
Intros; Unfold fOSC chobjsc_SC.
Elim (fOSC (objectSC s) o1).
Intro; Apply AddRemEq; Auto.
Auto.
Qed.
|
|
Lemma EqfOSC5:
(s:SFSstate; o:OBJECT; p:OBJNAME)
(FuncPre1 s)
->(FuncPre2 s)
->~(set_In (p,File) (domf (files s)))
->~(set_In (p,Directory) (domd (directories s)))
->p=(ObjName o)
->(None SecClass)=(fOSC (objectSC s) o).
Intros.
Symmetry; Unfold fOSC; Apply NotInDOMIsUndef.
Replace (DOM OBJeq_dec (objectSC s)) with (DOM OBJeq_dec (acl s)).
Rewrite H3 in H1; Rewrite H3 in H2.
Auto.
Qed.
|
|
Lemma EqfOSC1:
(s:SFSstate; o:OBJECT; p:OBJNAME; u:SUBJECT)
~p=(ObjName o)
->(fOSC (objectSC s) o)=(fOSC (create_oSC s u p) o).
Intros.
Unfold create_oSC.
Elim (fSSC (subjectSC s) u); Elim (fsecmat (secmat s) (MyDir p)).
Intros; Unfold fOSC; Apply AddEq.
Intro; Apply H.
Rewrite H0; Simpl; Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma EqfOSC2:
(s:SFSstate; o:OBJECT; p:OBJNAME; u:SUBJECT)
~p=(ObjName o)
->(fOSC (objectSC s) o)=(fOSC (mkdir_oSC s u p) o).
Intros.
Unfold mkdir_oSC.
Elim (fSSC (subjectSC s) u); Elim (fsecmat (secmat s) (MyDir p)).
Intros; Unfold fOSC; Apply AddEq.
Intro; Apply H.
Rewrite H0; Simpl; Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma EqfOSC3:
(s:SFSstate; o1,o2:OBJECT)
~o1=o2
->(fOSC (objectSC s) o2)=(fOSC (unlink_oSC s o1) o2).
Intros.
Unfold unlink_oSC.
Elim (fOSC (objectSC s) o1).
Intro; Unfold fOSC; Apply RemEq.
Auto.
Auto.
Qed.
|
|
Lemma Eqfacl1:
(s:SFSstate; o:OBJECT; p:OBJNAME; u:SUBJECT; perms:PERMS)
~p=(ObjName o)
->(facl (acl s) o)=(facl (create_acl s u p perms) o).
Intros.
Unfold create_acl.
Elim (fSSC (subjectSC s) u); Elim (fsecmat (secmat s) (MyDir p)).
Intros; Unfold facl; Apply AddEq.
Intro y1; Apply H; Rewrite y1; Simpl; Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma Eqfacl2:
(s:SFSstate; o:OBJECT; p:OBJNAME; u:SUBJECT; perms:PERMS)
~p=(ObjName o)
->(facl (acl s) o)=(facl (mkdir_acl s u p perms) o).
Intros.
Unfold mkdir_acl.
Elim (fSSC (subjectSC s) u); Elim (fsecmat (secmat s) (MyDir p)).
Intros; Unfold facl; Apply AddEq.
Intro y1; Apply H; Rewrite y1; Simpl; Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma Eqfacl3:
(s:SFSstate; o1,o2:OBJECT)
~o1=o2
->(facl (acl s) o2)=(facl (unlink_acl s o1) o2).
Intros.
Unfold unlink_acl.
Elim (facl (acl s) o1).
Intros; Unfold facl; Apply RemEq.
Auto.
Auto.
Qed.
|
|
Lemma Eqfacl4:
(s:SFSstate; o:OBJECT; y,z:AccessCtrlListData)
(FuncPre4 s)
->(facl (acl s) o)=(Some AccessCtrlListData y)
->(facl (rmdir_acl s o) o)=(Some AccessCtrlListData z)
->False.
Unfold facl.
Intros until z.
Cut Cases (PARTFUNC OBJeq_dec (acl s) o) of
(Some y) => (set_In (o,y) (acl s))
| None => ~(set_In o (DOM OBJeq_dec (acl s)))
end.
Unfold rmdir_acl.
Unfold facl.
Elim (PARTFUNC OBJeq_dec (acl s) o).
Intros.
Cut (PARTFUNC OBJeq_dec (set_remove ACLeq_dec (o,a) (acl s)) o)
=(None AccessCtrlListData).
Rewrite H2.
Intro.
Discriminate H3.
Auto.
Intros.
Discriminate H1.
Apply DOMFuncRel4.
Qed.
|
|
Lemma Eqfacl5:
(s:SFSstate; o:OBJECT; y,z:AccessCtrlListData)
(FuncPre4 s)
->(facl (acl s) o)=(Some AccessCtrlListData y)
->(facl (unlink_acl s o) o)=(Some AccessCtrlListData z)
->False.
Unfold facl.
Intros until z.
Cut Cases (PARTFUNC OBJeq_dec (acl s) o) of
(Some y) => (set_In (o,y) (acl s))
| None => ~(set_In o (DOM OBJeq_dec (acl s)))
end.
Unfold unlink_acl.
Unfold facl.
Elim (PARTFUNC OBJeq_dec (acl s) o).
Intros.
Cut (PARTFUNC OBJeq_dec (set_remove ACLeq_dec (o,a) (acl s)) o)
=(None AccessCtrlListData).
Rewrite H2.
Intro.
Discriminate H3.
Auto.
Intros.
Discriminate H1.
Apply DOMFuncRel4.
Qed.
|
|
Lemma EqfOSC4:
(s:SFSstate; o:OBJECT; y,z:SecClass)
(FuncPre6 s)
->(fOSC (objectSC s) o)=(Some SecClass y)
->(fOSC (rmdir_oSC s o) o)=(Some SecClass z)
->False.
Unfold fOSC.
Intros until z.
Cut Cases (PARTFUNC OBJeq_dec (objectSC s) o) of
(Some y) => (set_In (o,y) (objectSC s))
| None => ~(set_In o (DOM OBJeq_dec (objectSC s)))
end.
Unfold rmdir_oSC.
Unfold fOSC.
Elim (PARTFUNC OBJeq_dec (objectSC s) o).
Intros.
Cut (PARTFUNC OBJeq_dec (set_remove OSCeq_dec (o,a) (objectSC s)) o)
=(None SecClass).
Rewrite H2.
Intro.
Discriminate H3.
Auto.
Intros.
Discriminate H1.
Apply DOMFuncRel4.
Qed.
|
|
Lemma EqfOSC7:
(s:SFSstate; o:OBJECT; y,z:SecClass)
(FuncPre6 s)
->(fOSC (objectSC s) o)=(Some SecClass y)
->(fOSC (unlink_oSC s o) o)=(Some SecClass z)
->False.
Unfold fOSC.
Intros until z.
Cut Cases (PARTFUNC OBJeq_dec (objectSC s) o) of
(Some y) => (set_In (o,y) (objectSC s))
| None => ~(set_In o (DOM OBJeq_dec (objectSC s)))
end.
Unfold unlink_oSC.
Unfold fOSC.
Elim (PARTFUNC OBJeq_dec (objectSC s) o).
Intros.
Cut (PARTFUNC OBJeq_dec (set_remove OSCeq_dec (o,a) (objectSC s)) o)
=(None SecClass).
Rewrite H2.
Intro.
Discriminate H3.
Auto.
Intros.
Discriminate H1.
Apply DOMFuncRel4.
Qed.
|
|
Lemma NoDACChange:
(s:SFSstate; o:OBJECT; SSC:(set SUBJECT*SecClass);
OSC:(set OBJECT*SecClass); FILES:(set OBJECT*FILECONT);
DIRECTS:(set OBJECT*DIRCONT); SM:(set OBJECT*ReadersWriters))
~(DACCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) SSC (AllGrp s)
(RootGrp s) (SecAdmGrp s) OSC (acl s) SM FILES DIRECTS) o).
Intros.
Intro.
Inversion H; Simpl in H1; Cut y=z.
Intro EQ; Rewrite EQ in H2; Inversion H2; Auto.
Rewrite H0 in H1; Injection H1; Auto.
Intro EQ; Rewrite EQ in H2; Inversion H2; Auto.
Rewrite H0 in H1; Injection H1; Auto.
Qed.
|
|
Lemma NoDACChange2:
(s:SFSstate; o:OBJECT)~(DACCtrlAttrHaveChanged s s o).
Intros; Intro;
EApply (NoDACChange s o (subjectSC s) (objectSC s) (files s)
(directories s) (secmat s)).
Generalize H; Elim s; Simpl; Auto.
Qed.
|
|
Lemma NoMACObjChange:
(s:SFSstate; o:OBJECT; FILES:(set OBJECT*FILECONT);
DIRECTS:(set OBJECT*DIRCONT); ACL:(set OBJECT*AccessCtrlListData);
SSC:(set SUBJECT*SecClass); SM:(set OBJECT*ReadersWriters))
~(MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) SSC (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) ACL SM FILES DIRECTS) o).
Intros; Intro.
Inversion H; Simpl in H1.
Cut x=y.
Intro EQ; Rewrite EQ in H2; Inversion H2; Auto.
Rewrite H0 in H1; Injection H1; Auto.
Qed.
|
|
Lemma NoMACObjChange2:
(s:SFSstate; o:OBJECT)~(MACObjCtrlAttrHaveChanged s s o).
Intros; Intro;
EApply (NoMACObjChange s o (files s) (directories s) (acl s)
(subjectSC s) (secmat s)).
Generalize H; Elim s; Simpl; Auto.
Qed.
|
|
Lemma NoMACSubChange:
(s:SFSstate; u:SUBJECT; ACL: (set OBJECT*AccessCtrlListData);
OSC:(set OBJECT*SecClass); FILES:(set OBJECT*FILECONT);
DIRECTS:(set OBJECT*DIRCONT); SM:(set OBJECT*ReadersWriters))
~(MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) OSC ACL SM FILES DIRECTS) u).
Intros; Intro; Inversion H.
Simpl in H1.
Cut x=y.
Intro EQ; Rewrite EQ in H2; Inversion H2; Auto.
Rewrite H0 in H1; Injection H1; Auto.
Qed.
|
|
Lemma NoMACSubChange2:
(s:SFSstate; u:SUBJECT)~(MACSubCtrlAttrHaveChanged s s u).
Intros; Intro;
EApply (NoMACSubChange s u (acl s) (objectSC s) (files s) (directories s) (secmat s)).
Generalize H; Elim s; Simpl; Auto.
Qed.
|
|
Lemma eq_scSym: (a,b:SecClass)(eq_sc a b)->(eq_sc b a).
Unfold eq_sc; Intros.
Elim H; Intros.
Rewrite H0; Rewrite H1.
Auto.
Qed.
|
|
Lemma ChsubscPSS1:
(s:SFSstate; u:SUBJECT; y:ReadersWriters)
((rw:ReadersWriters)
~(set_In u (ActReaders rw))/\~(set_In u (ActWriters rw)))
->~((set_In u (ActReaders y))\/(set_In u (ActWriters y))).
Intros.
Cut ~(set_In u (ActReaders y))/\~(set_In u (ActWriters y)).
Tauto.
Auto.
Qed.
|
|
Lemma EqfSSC1:
(s:SFSstate; u,u0:SUBJECT; sc:SecClass)
~u=u0 -> (fSSC (subjectSC s) u0)=(fSSC (chsubsc_SC s u sc) u0).
Intros; Unfold chsubsc_SC.
Elim (fSSC (subjectSC s) u).
Intros; Unfold fSSC; Apply AddRemEq; Auto.
Auto.
Qed.
|
|
Lemma Close_smCorr:
(s:SFSstate; Sub:SUBJECT; o:OBJECT)
(FuncPre5 s)
->Cases (fsecmat (secmat s) o) of
|(Some y) =>
(set_In Sub
(set_union SUBeq_dec (ActReaders y) (ActWriters y)))
|None => False
end
->Cases (fsecmat (close_sm s Sub o) o) of
|None =>True
|(Some y) =>~(set_In Sub (ActReaders y))/\~(set_In Sub (ActWriters y))
end.
Intros until o.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold close_sm.
Elim (fsecmat (secmat s) o); Intros.
Elim (set_remove SUBeq_dec Sub (ActReaders a));
Elim (set_remove SUBeq_dec Sub (ActWriters a)).
Replace (fsecmat (set_remove SECMATeq_dec (o,a) (secmat s)) o)
with (None ReadersWriters).
Auto.
Symmetry; Unfold fsecmat; Unfold FuncPre5 in H0; Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl; Split; Apply Set_remove1.
Unfold fsecmat; Apply AddEq1.
Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl; Split; Apply Set_remove1.
Unfold fsecmat; Apply AddEq1.
Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl; Split; Apply Set_remove1.
Unfold fsecmat; Apply AddEq1.
Auto.
Tauto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Close_smCorr2:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT)
(FuncPre5 s)
->Cases (fsecmat (secmat s) o) of
|(Some y) =>
(set_In Sub
(set_union SUBeq_dec (ActReaders y) (ActWriters y)))
|None => False
end
->Cases (fsecmat (close_sm s Sub o) o) (fsecmat (secmat s) o) of
| _ None => False
| None (Some z) => True
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Intros until o.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold close_sm.
Elim (fsecmat (secmat s) o); Intros.
Elim (set_remove SUBeq_dec Sub (ActReaders a));
Elim (set_remove SUBeq_dec Sub (ActWriters a)).
Replace (fsecmat (set_remove SECMATeq_dec (o,a) (secmat s)) o)
with (None ReadersWriters).
Auto.
Symmetry; Unfold fsecmat; Unfold FuncPre5 in H; Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRW Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRW Sub o a)).
Unfold NEWRW; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Tauto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Eqfsecmat1:
(s:SFSstate; o1,o2:OBJECT; u:SUBJECT)
~o1=o2 -> (fsecmat (secmat s) o2)=(fsecmat (close_sm s u o1) o2).
Unfold close_sm fsecmat; Intros;
Elim (PARTFUNC OBJeq_dec (secmat s) o1).
Intro; Elim (set_remove SUBeq_dec u (ActReaders a));
Elim (set_remove SUBeq_dec u (ActWriters a)).
Auto.
Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma Close_smCorr3:
(s:SFSstate; Sub:SUBJECT; o:OBJECT)
(fsecmat (secmat s) o)=(None ReadersWriters)
->(fsecmat (close_sm s Sub o) o)=(None ReadersWriters).
Intros until o; Unfold close_sm.
Intro.
Generalize H.
Elim (fsecmat (secmat s) o).
Intros y H0; Discriminate H0.
Auto.
Qed.
|
|
Lemma OwnerClose_smCorr2:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT)
(FuncPre5 s)
->Cases (fsecmat (secmat s) o) of
|(Some y) =>
(set_In Sub
(set_union SUBeq_dec (ActReaders y) (ActWriters y)))
|None => False
end
->Cases (fsecmat (ownerclose_sm s Sub o) o) (fsecmat (secmat s) o) of
| _ None => False
| None (Some z) => True
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Intros until o.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold ownerclose_sm.
Elim (fsecmat (secmat s) o); Intros.
Elim (set_remove SUBeq_dec Sub (ActReaders a));
Elim (set_remove SUBeq_dec Sub (ActWriters a)).
Replace (fsecmat (set_remove SECMATeq_dec (o,a) (secmat s)) o)
with (None ReadersWriters).
Auto.
Symmetry; Unfold fsecmat; Unfold FuncPre5 in H0; Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRWOC Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRWOC Sub o a)).
Unfold NEWRWOC; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRWOC Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRWOC Sub o a)).
Unfold NEWRWOC; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Intros.
Replace (fsecmat
(set_add SECMATeq_dec (o,(NEWRWOC Sub o a))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters (NEWRWOC Sub o a)).
Unfold NEWRWOC; Simpl.
Split;
[ Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActReaders a) 4!u0
5!Sub); Auto
| Intro;
EApply (Set_remove2 1!SUBJECT 2!SUBeq_dec 3!(ActWriters a) 4!u0
5!Sub); Auto ].
Unfold fsecmat; Apply AddEq1.
Auto.
Tauto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Eqfsecmat2:
(s:SFSstate; o1,o2:OBJECT; u:SUBJECT)
~o1=o2 -> (fsecmat (secmat s) o2)=(fsecmat (ownerclose_sm s u o1) o2).
Unfold ownerclose_sm fsecmat; Intros;
Elim (PARTFUNC OBJeq_dec (secmat s) o1).
Intro; Elim (set_remove SUBeq_dec u (ActReaders a));
Elim (set_remove SUBeq_dec u (ActWriters a)).
Auto.
Auto.
Auto.
Auto.
Auto.
Qed.
|
|
Lemma OwnerClose_smCorr3:
(s:SFSstate; Sub:SUBJECT; o:OBJECT)
(fsecmat (secmat s) o)=(None ReadersWriters)
->(fsecmat (ownerclose_sm s Sub o) o)=(None ReadersWriters).
Intros until o; Unfold ownerclose_sm.
Intro.
Generalize H.
Elim (fsecmat (secmat s) o).
Intros y H0; Discriminate H0.
Auto.
Qed.
|
|
Lemma Open_smCorr3:
(s:SFSstate; Sub:SUBJECT; o:OBJECT; m:MODE)
(FuncPre5 s)
->(fsecmat (open_sm s Sub o m) o)=(None ReadersWriters)
->(fsecmat (secmat s) o)=(None ReadersWriters).
Intros until m; Intro; Unfold open_sm.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Elim m; Elim (fsecmat (secmat s) o).
Intro; Intro;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (ActReaders a))
(ActWriters a)))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))).
Intros H2; Discriminate H2.
Unfold fsecmat; Apply AddEq1; Auto.
Intro;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))) (secmat s)) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))).
Intro H2; Discriminate H2.
Unfold fsecmat; Apply AddEq1; Auto.
Intro; Intro;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (ActReaders a)
(set_add SUBeq_dec Sub (ActWriters a))))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))).
Intro H2; Discriminate H2.
Unfold fsecmat; Apply AddEq1; Auto.
Intro;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT))))
(secmat s)) o)
with (Some ReadersWriters
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT)))).
Intro H2; Discriminate H2.
Unfold fsecmat; Apply AddEq1; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Open_smCorr21:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT; m:MODE)
~Sub=u0
->(FuncPre5 s)
->Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold open_sm.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (ActReaders a))
(ActWriters a)))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))).
Simpl.
Split; (Intros; EAuto).
Unfold fsecmat; Apply AddEq1; Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))) (secmat s)) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))).
Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Open_smCorr22:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT; m:MODE)
~Sub=u0
->(FuncPre5 s)
->Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
/\((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold open_sm.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (ActReaders a)
(set_add SUBeq_dec Sub (ActWriters a))))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))).
Simpl.
Split; (Intro; EAuto).
Unfold fsecmat; Apply AddEq1; Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT))))
(secmat s)) o)
with (Some ReadersWriters
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT)))).
Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Eqfsecmat3:
(s:SFSstate; o1,o2:OBJECT; u:SUBJECT; m:MODE)
~o1=o2 -> (fsecmat (secmat s) o2)=(fsecmat (open_sm s u o1 m) o2).
Intros until m; Unfold fsecmat open_sm.
Elim m; Elim (fsecmat (secmat s) o1).
Intros; Apply AddRemEq; Auto.
Intros; Apply AddEq; Auto.
Intros; Apply AddRemEq; Auto.
Intros; Apply AddEq; Auto.
Qed.
|
|
Lemma Chobjsc_Corr:
(s:SFSstate; o:OBJECT; sc:SecClass)
(FuncPre6 s)
->((fOSC (objectSC s) o)=(None SecClass)
<->(fOSC (chobjsc_SC s o sc) o)=(None SecClass)).
Intros; Unfold chobjsc_SC.
Cut Cases (fOSC (objectSC s) o) of
(Some y) => (set_In (o,y) (objectSC s))
| None => ~(set_In o (DOM OBJeq_dec (objectSC s)))
end.
Split.
Intro H1; Rewrite H1; Auto.
Generalize H0; Elim (fOSC (objectSC s) o).
Intro; Intro;
Replace (fOSC
(set_add OSCeq_dec (o,sc)
(set_remove OSCeq_dec (o,a) (objectSC s))) o)
with (Some SecClass sc).
Intro H2; Discriminate H2.
Unfold fOSC; Apply AddEq1.
Auto.
Auto.
Unfold fOSC; Apply DOMFuncRel4.
Qed.
|
|
Lemma Aux1:
(y:SecClass)
~((Some SecClass y)=(None SecClass)
<->(None SecClass)=(None SecClass)).
Intro; Unfold iff; Intro H; Elim H; Intros.
Absurd (Some SecClass y)=(None SecClass); Auto.
Intro D; Discriminate D.
Qed.
|
|
Lemma Chsubsc_Corr:
(s:SFSstate; u:SUBJECT; sc:SecClass)
(FuncPre7 s)
->((fSSC (subjectSC s) u)=(None SecClass)
<->(fSSC (chsubsc_SC s u sc) u)=(None SecClass)).
Intros; Unfold chsubsc_SC.
Cut Cases (fSSC (subjectSC s) u) of
(Some y) => (set_In (u,y) (subjectSC s))
| None => ~(set_In u (DOM SUBeq_dec (subjectSC s)))
end.
Split.
Intro H1; Rewrite H1; Auto.
Generalize H0; Elim (fSSC (subjectSC s) u).
Intro; Intro;
Replace (fSSC
(set_add SSCeq_dec (u,sc)
(set_remove SSCeq_dec (u,a) (subjectSC s))) u)
with (Some SecClass sc).
Intro H2; Discriminate H2.
Unfold fSSC; Apply AddEq1; Auto.
Auto.
Auto.
Unfold fSSC; Apply DOMFuncRel4.
Qed.
|
|
Lemma Open_smCorr31:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT; m:MODE)
(FuncPre5 s)
->Cases (fsecmat (open_sm s Sub o READ) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActReaders y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActWriters y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActWriters y))->(set_In u0 (ActWriters z)))
end.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold open_sm.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (ActReaders a))
(ActWriters a)))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))).
Simpl; Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))) (secmat s)) o)
with (Some ReadersWriters
(mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT))
(empty_set SUBJECT))).
Simpl; Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Lemma Open_smCorr32:
(s:SFSstate; Sub,u0:SUBJECT; o:OBJECT; m:MODE)
(FuncPre5 s)
->Cases (fsecmat (open_sm s Sub o WRITE) o) (fsecmat (secmat s) o) of
(Some y) None =>
(ActWriters y)=(set_add SUBeq_dec Sub (empty_set SUBJECT))
/\(ActReaders y)=(empty_set SUBJECT)
| None _ => False
| (Some y) (Some z) =>
((set_In u0 (ActReaders y))->(set_In u0 (ActReaders z)))
end.
Intros.
Cut Cases (fsecmat (secmat s) o) of
(Some y) => (set_In (o,y) (secmat s))
| None => ~(set_In o (DOM OBJeq_dec (secmat s)))
end.
Unfold open_sm.
Elim (fsecmat (secmat s) o).
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (ActReaders a)
(set_add SUBeq_dec Sub (ActWriters a))))
(set_remove SECMATeq_dec (o,a) (secmat s))) o)
with (Some ReadersWriters
(mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))).
Simpl; Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Intros;
Replace (fsecmat
(set_add SECMATeq_dec
(o,
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT))))
(secmat s)) o)
with (Some ReadersWriters
(mkRW (empty_set SUBJECT)
(set_add SUBeq_dec Sub (empty_set SUBJECT)))).
Simpl; Auto.
Unfold fsecmat; Apply AddEq1; Auto.
Unfold fsecmat; Apply DOMFuncRel4.
Qed.
|
|
Hints Resolve eq_scIMPLYle_sc eq_scSym Eqfsecmat1 Close_smCorr3
TwoImpLeft TwoImpRight EqfOSC1 ChsubscPSS1 Eqfsecmat2
NoMACObjChange NoDACChange NoMACSubChange EqfOSC6
Eqfacl1 Eqfacl2 Eqfacl3 EqfOSC1 EqfOSC2 EqfOSC3 Aux1
NotInDOMIsUndef2 Eqfacl4 EqfOSC4 EqfOSC5 EqfSSC1
OwnerClose_smCorr3 Open_smCorr3 Eqfsecmat3 Chobjsc_Corr
NoMACObjChange2 NoDACChange2 NoMACSubChange2
Chsubsc_Corr NotInDOMIsUndef3 Eqfacl5 EqfOSC7.