Verification: close |
Require ModelProperties.
Require AuxiliaryLemmas.
Section closeIsSecure.
|
|
Lemma ClosePSS:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(SecureState s)->(TransFunc u s Close t)->(SecureState t).
Intros s t Sub FP5 SS TF; Inversion TF.
Inversion H.
Unfold SecureState.
BreakSS.
Split.
Unfold DACSecureState; Intros; Simpl.
Elim (OBJeq_dec o o0); Intro y0.
Rewrite <- y0.
Elim (SUBeq_dec Sub u0); Intro y1.
Rewrite <- y1.
Cut Cases (fsecmat (close_sm s Sub o) o) of
None => True
| (Some y) =>
~(set_In Sub (ActReaders y))/\~(set_In Sub (ActWriters y))
end.
Elim (fsecmat (close_sm s Sub o) o).
Intros; Split; Intro; Tauto.
Auto.
Apply Close_smCorr; Auto.
Cut 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.
Cut Cases (fsecmat (secmat s) o) of
None => True
| (Some y) =>
((set_In u0 (ActReaders y))->(PreDACRead s u0 o))
/\((set_In u0 (ActWriters y))->(PreDACWrite s u0 o))
end.
Unfold 3 4 close_sm PreDACRead PreDACWrite; Simpl;
Elim (fsecmat (secmat s) o); Elim (fsecmat (close_sm s Sub o) o).
Intros.
Elim H6; Elim H5; Intros.
Split; Intro.
Apply H7; Apply H9; Auto.
Apply H8; Apply H10; Auto.
Auto.
Tauto.
Auto.
Unfold DACSecureState in DAC; Apply DAC.
Apply Close_smCorr2; Auto.
Replace (fsecmat (close_sm s Sub o) o0) with (fsecmat (secmat s) o0).
Unfold close_sm PreDACRead PreDACWrite; Simpl;
Unfold DACSecureState PreDACRead PreDACWrite in DAC; Apply DAC.
Auto.
Unfold SimpleSecurity; Intros; Simpl.
Elim (OBJeq_dec o o0); Intro y0.
Rewrite <- y0.
Cut 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.
Cut Cases
(fsecmat (secmat s) o)
(fOSC (objectSC s) o)
(fSSC (subjectSC s) u0)
of
None _ _ => True
| _ None _ => True
| _ _ None => True
| (Some x) (Some y) (Some z) =>
(set_In u0 (ActReaders x))\/(set_In u0 (ActWriters x))
->(le_sc y z)
end.
Elim (fsecmat (secmat s) o); Elim (fsecmat (close_sm s Sub o) o);
Elim (fOSC (objectSC s) o); Elim (fSSC (subjectSC s) u0);
Contradiction Orelse Trivial.
Tauto.
Unfold SimpleSecurity in MAC; Apply MAC.
Apply Close_smCorr2; Auto.
Replace (fsecmat (close_sm s Sub o) o0) with (fsecmat (secmat s) o0).
Unfold SimpleSecurity in MAC; Apply MAC.
Auto.
Qed.
|
|
Lemma ClosePSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(StarProperty s)->(TransFunc u s Close t)->(StarProperty t).
Intros s t Sub FP5 SP TF; Inversion TF.
Inversion H.
Unfold StarProperty; Simpl; Intros.
Cut Cases
(fsecmat (secmat s) o1)
(fsecmat (secmat s) o2)
(fOSC (objectSC s) o2)
(fOSC (objectSC s) o1)
of
None _ _ _ => True
| _ None _ _ => True
| _ _ None _ => True
| _ _ _ None => True
| (Some w) (Some x) (Some y) (Some z) =>
(set_In u0 (ActWriters w))
->(set_In u0 (ActReaders x))
->(le_sc y z)
end.
Cut 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.
Elim (OBJeq_dec o o1); Elim (OBJeq_dec o o2); Intros EQ2 EQ1.
Rewrite <- EQ1; Rewrite <- EQ2.
Elim (fsecmat (secmat s) o); Elim (fOSC (objectSC s) o);
Elim (fsecmat (close_sm s Sub o) o); Intros; Auto.
Replace (fsecmat (close_sm s Sub o) o2) with (fsecmat (secmat s) o2).
Rewrite <- EQ1.
Elim (fsecmat (secmat s) o2); Elim (fOSC (objectSC s) o);
Elim (fOSC (objectSC s) o2); Elim (fsecmat (secmat s) o);
Elim (fsecmat (close_sm s Sub o) o); Intros;
Contradiction Orelse Auto.
Tauto.
Auto.
Replace (fsecmat (close_sm s Sub o) o1) with (fsecmat (secmat s) o1).
Rewrite <- EQ2.
Elim (fsecmat (secmat s) o1); Elim (fOSC (objectSC s) o);
Elim (fOSC (objectSC s) o1); Elim (fsecmat (secmat s) o);
Elim (fsecmat (close_sm s Sub o) o); Intros;
Contradiction Orelse Auto.
Tauto.
Auto.
Replace (fsecmat (close_sm s Sub o) o2) with (fsecmat (secmat s) o2).
Replace (fsecmat (close_sm s Sub o) o1) with (fsecmat (secmat s) o1).
Auto.
Auto.
Auto.
Apply Close_smCorr2; Auto.
Unfold StarProperty in SP; Apply SP.
Qed.
|
|
Lemma ClosePCP:
(s,t:SFSstate)(PreservesControlProp s Close t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intros;
Absurd (DACCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(close_sm s Sub o) (files s) (directories s)) o0);
Auto.
Intros;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(close_sm s Sub o) (files s) (directories s)) o0);
Auto.
Intros;
Absurd (MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
(close_sm s Sub o) (files s) (directories s)) u0);
Auto.
Qed.
End closeIsSecure.
Hints Resolve ClosePSS ClosePSP ClosePCP.