Verification: aclstat |
Require
ModelProperties.
Require
AuxiliaryLemmas.
Section
aclstatIsSecure.
|
Lemma
AclstatPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s Aclstat t)->(SecureState t).
OpDontChangeStPSS.
Qed
.
|
Lemma
AclstatPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Aclstat t)->(StarProperty t).
OpDontChangeStPSP.
Qed
.
|
Lemma
AclstatPCP:
(s,t:SFSstate)(PreservesControlProp s Aclstat t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Split.
Intros.
Split.
Intros; Absurd (DACCtrlAttrHaveChanged t t o0); Auto.
Intro; Absurd (MACObjCtrlAttrHaveChanged t t o0); Auto.
Intros; Absurd (MACSubCtrlAttrHaveChanged t t u0); Auto.
Qed
.
End
aclstatIsSecure.
Hints
Resolve AclstatPSS AclstatPSP AclstatPCP.