Verification: delUsrGrpFromAcl



Lemma DelUsrGrpFromAclPSS:
 (s,t:SFSstate; u:SUBJECT)
  (SecureState s)->(TransFunc u s DelUsrGrpFromAcl 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.
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 delUsrGrpFromAcl_acl.
Simpl.
Elim (facl (acl s) o).
Intro.
Replace (facl
  (set_add ACLeq_dec
    (o,
     (acldata
       Cases (SUBeq_dec (owner a) pu) of
         (left _) => root
       | (right _) => (owner a)
       end (group a)
       (set_remove SUBeq_dec ru (UsersReaders a))
       (set_remove GRPeq_dec rg (GroupReaders a))
       (set_remove SUBeq_dec wu (UsersWriters a))
       (set_remove GRPeq_dec wg (GroupWriters a))
       Cases (SUBeq_dec (owner a) pu) of
         (left _) =>
          (set_add SUBeq_dec root
            (set_remove SUBeq_dec pu (UsersOwners a)))
       | (right _) =>
          (set_remove SUBeq_dec pu (UsersOwners a))
       end (set_remove 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.

Tauto.

Split.
Apply ReadWriteImpRead.
Auto.

Apply ReadWriteImpWrite.
Auto.

Auto.

Qed.



Lemma DelUsrGrpFromAclPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s DelUsrGrpFromAcl t)->(StarProperty t).
StartPSP.
Inversion H; Auto.
Qed.



Lemma DelUsrGrpFromAclPCP:
    (s,t:SFSstate)(PreservesControlProp s DelUsrGrpFromAcl t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
  Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Inversion H7.
Simpl in H9.
Elim (OBJeq_dec o o0); Intro y0.
Rewrite <- y0; Auto.

Cut y=z.
Intro.
Cut False.
Tauto.

Rewrite H11 in H10; Inversion H10; Auto.

Cut (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0)
     =(facl (acl s) o0).
Intro H13; Rewrite H13 in H9; Rewrite H8 in H9; Injection H9; Auto.

Symmetry.
Unfold delUsrGrpFromAcl_acl.
Elim (facl (acl s) o).
Intro; Unfold facl; Apply AddRemEq.
Auto.

Auto.

Simpl in H9.
Elim (OBJeq_dec o o0); Intro.
Rewrite <- a; Auto.

Cut y=z.
Intro.
Cut False.
Tauto.

Rewrite H11 in H10; Inversion H10; Auto.

Cut (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0)
     =(facl (acl s) o0).
Intro H12; Rewrite H12 in H9; Rewrite H8 in H9; Injection H9; Auto.

Symmetry.
Unfold delUsrGrpFromAcl_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)
             (delUsrGrpFromAcl_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)
             (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s)
             (files s) (directories s)) u0);
  Auto.

Qed.


End delUsrGrpFromAclIsSecure.

Hints Resolve DelUsrGrpFromAclPSS DelUsrGrpFromAclPSP
              DelUsrGrpFromAclPCP.