Verification: addUsrGrpToAcl |
Require ModelProperties.
Require AuxiliaryLemmas.
Section addUsrGrpToAclIsSecure.
|
|
Lemma AddUsrGrpToAclPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s AddUsrGrpToAcl t)->(SecureState t).
StartPSS .
Inversion H.
Unfold SecureState.
BreakSS .
Split.
Unfold DACSecureState.
Simpl.
Intros.
Elim (OBJeq_dec o o0).
Intro.
Rewrite <- a.
Cut (fsecmat (secmat s) o)=(None ReadersWriters).
Intro H7.
Rewrite H7.
EAuto.
Unfold fsecmat.
Auto.
Intro.
Cut (Cases (fsecmat (secmat s) o0) of
(Some y) =>
((set_In u0 (ActReaders y))->(PreDACRead s u0 o0))
| None => True
end)
/\
(Cases (fsecmat (secmat s) o0) of
(Some y) =>
((set_In u0 (ActWriters y))->(PreDACWrite s u0 o0))
| None => True
end).
Elim (fsecmat (secmat s) o0).
Unfold PreDACRead PreDACWrite addUsrGrpToAcl_acl.
Simpl.
Elim (facl (acl s) o).
Intro.
Replace (facl
(set_add ACLeq_dec
(o,
(acldata (owner a) (group a)
(set_add SUBeq_dec ru (UsersReaders a))
(set_add GRPeq_dec rg (GroupReaders a))
(set_add SUBeq_dec wu (UsersWriters a))
(set_add GRPeq_dec wg (GroupWriters a))
(set_add SUBeq_dec pu (UsersOwners a))
(set_add GRPeq_dec pg (GroupOwners a))))
(set_remove ACLeq_dec (o,a) (acl s))) o0)
with (facl (acl s) o0).
Elim (facl (acl s) o0).
Auto.
Auto.
Unfold facl.
Auto.
Auto.
Trivial.
Split.
Apply ReadWriteImpRead.
Auto.
Apply ReadWriteImpWrite.
Auto.
Auto.
Qed.
|
|
Lemma AddUsrGrpToAclPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s AddUsrGrpToAcl t)->(StarProperty t).
StartPSP.
Inversion H; Auto.
Qed.
|
|
Lemma AddUsrGrpToAclPCP:
(s,t:SFSstate)(PreservesControlProp s AddUsrGrpToAcl t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Inversion H6.
Simpl in H8.
Elim (OBJeq_dec o o0); Intro.
Rewrite <- a; Auto.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H10 in H9; Inversion H9; Auto.
Cut (facl (addUsrGrpToAcl_acl s o ru wu pu rg wg pg) o0)
=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold addUsrGrpToAcl_acl.
Elim (facl (acl s) o).
Intro; Unfold facl; Apply AddRemEq.
Auto.
Auto.
Simpl in H8.
Elim (OBJeq_dec o o0); Intro.
Rewrite <- a; Auto.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H10 in H9; Inversion H9; Auto.
Cut (facl (addUsrGrpToAcl_acl s o ru wu pu rg wg pg) o0)
=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold addUsrGrpToAcl_acl.
Elim (facl (acl s) o).
Intro; Unfold facl; Apply AddRemEq.
Auto.
Auto.
Intro;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s)
(addUsrGrpToAcl_acl s o ru wu pu rg wg pg) (secmat s)
(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)
(addUsrGrpToAcl_acl s o ru wu pu rg wg pg) (secmat s)
(files s) (directories s)) u0);
Auto.
Qed.
End addUsrGrpToAclIsSecure.
Hints Resolve AddUsrGrpToAclPSS AddUsrGrpToAclPSP AddUsrGrpToAclPCP.