Verification: sscstat |
Require ModelProperties.
Require AuxiliaryLemmas.
Section sscstatIsSecure.
|
|
Lemma SscstatPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s Sscstat t)->(SecureState t).
OpDontChangeStPSS.
Qed.
|
|
Lemma SscstatPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Sscstat t)->(StarProperty t).
OpDontChangeStPSP.
Qed.
|
|
Lemma SscstatPCP:
(s,t:SFSstate)(PreservesControlProp s Sscstat t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Split.
Intros.
Split.
Intro.
Absurd (DACCtrlAttrHaveChanged t t o); Auto.
Intro; Absurd (MACObjCtrlAttrHaveChanged t t o); Auto.
Intros; Absurd (MACSubCtrlAttrHaveChanged t t u0); Auto.
Qed.
End sscstatIsSecure.
Hints Resolve SscstatPSS SscstatPSP SscstatPCP.