Verification: chobjsc |
Require ModelProperties.
Require AuxiliaryLemmas.
Section chobjscIsSecure.
|
|
Lemma ChobjscPSS:
(s,t:SFSstate; u:SUBJECT)
(FuncPre6 s)
->(SecureState s)->(TransFunc u s Chobjsc t)->(SecureState t).
Intros s t Sub FP6 SS TF; Inversion TF.
Inversion H.
Unfold SecureState.
BreakSS .
Split.
Auto.
Unfold SimpleSecurity; Simpl; Intros.
Elim (OBJeq_dec o o0).
Intro.
Rewrite <- a.
Cut (fsecmat (secmat s) o)=(None ReadersWriters).
Intro.
Rewrite H6.
Elim (fOSC (objectSC s) o); Elim (fOSC (chobjsc_SC s o sc) o);
Elim (fSSC (subjectSC s) u); Contradiction Orelse Auto.
Unfold fsecmat; Auto.
Intro.
Replace (fOSC (chobjsc_SC s o sc) o0) with (fOSC (objectSC s) o0).
Unfold SimpleSecurity in MAC; Apply MAC.
Auto.
Qed.
|
|
Lemma ChobjscPSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre6 s)
->(StarProperty s)->(TransFunc u s Chobjsc t)->(StarProperty t).
Intros s t Sub FP6 SP TF; Inversion TF.
Inversion H.
Unfold StarProperty; Simpl; Intros.
Elim (OBJeq_dec o o1); Elim (OBJeq_dec o o2); Intros EQ2 EQ1.
Rewrite <- EQ1; Rewrite <- EQ2.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Elim (fOSC (objectSC s) o); Elim (fOSC (chobjsc_SC s o sc) o);
Contradiction Orelse Auto.
Symmetry; Unfold fsecmat; Auto.
Auto.
Rewrite <- EQ1.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Replace (fOSC (chobjsc_SC s o sc) o2) with (fOSC (objectSC s) o2).
Elim (fsecmat (secmat s) o2); Elim (fOSC (chobjsc_SC s o sc) o);
Elim (fOSC (objectSC s) o); Elim (fOSC (objectSC s) o2); Intros;
Contradiction Orelse Auto.
Auto.
Symmetry; Unfold fsecmat; Auto.
Rewrite <- EQ2.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Replace (fOSC (chobjsc_SC s o sc) o1) with (fOSC (objectSC s) o1).
Elim (fsecmat (secmat s) o1); Elim (fOSC (chobjsc_SC s o sc) o);
Elim (fOSC (objectSC s) o); Elim (fOSC (objectSC s) o1); Intros;
Contradiction Orelse Auto.
Auto.
Symmetry; Unfold fsecmat; Auto.
Replace (fOSC (chobjsc_SC s o sc) o2) with (fOSC (objectSC s) o2).
Replace (fOSC (chobjsc_SC s o sc) o1) with (fOSC (objectSC s) o1).
Unfold StarProperty in SP; Apply SP.
Auto.
Auto.
Qed.
|
|
Lemma ChobjscPCP:
(s,t:SFSstate)(PreservesControlProp s Chobjsc t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Absurd (DACCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s)
(secmat s) (files s) (directories s)) o0); Auto.
Auto.
Intros.
Absurd (MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s)
(secmat s) (files s) (directories s)) u0); Auto.
Qed.
End chobjscIsSecure.
Hints Resolve ChobjscPSS ChobjscPSP ChobjscPCP.