Verification: chsubsc |
Require ModelProperties.
Require AuxiliaryLemmas.
Section chsubscIsSecure.
|
|
Lemma ChsubscPSS:
(s,t:SFSstate; u:SUBJECT)
(FuncPre7 s)
->(SecureState s)->(TransFunc u s Chsubsc t)->(SecureState t).
Intros s t Sub FP7 SS TF; Inversion TF.
Inversion H.
Unfold SecureState.
BreakSS .
Split.
Auto.
Unfold SimpleSecurity; Simpl.
Intros; Elim (SUBeq_dec u u0); Intro y0.
Rewrite <- y0.
Elim (fsecmat (secmat s) o); Elim (fSSC (chsubsc_SC s u sc) u);
Elim (fOSC (objectSC s) o); (Intros; Contradiction Orelse Auto).
Absurd (set_In u (ActReaders a1))\/(set_In u (ActWriters a1)); Auto.
Replace (fSSC (chsubsc_SC s u sc) u0) with (fSSC (subjectSC s) u0).
Unfold SimpleSecurity in MAC; Apply MAC; Auto.
Auto.
Qed.
|
|
Lemma ChsubscPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Chsubsc t)->(StarProperty t).
StartPSP.
Inversion H.
Auto.
Qed.
|
|
Lemma ChsubscPCP:
(s,t:SFSstate)(PreservesControlProp s Chsubsc 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) (chsubsc_SC s u sc)
(AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (
acl s) (secmat s) (files s) (directories s)) o); Auto.
Intro;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc)
(AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (
acl s) (secmat s) (files s) (directories s)) o); Auto.
Auto.
Qed.
End chsubscIsSecure.
Hints Resolve ChsubscPSS ChsubscPSP ChsubscPCP.