Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section chownIsSecure. 
 
Lemma ChownPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 SecureState s -> TransFunc u s Chown t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : SecureState s) (_ : TransFunc u s Chown t), SecureState t *)
StartPSS. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: SecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
unfold SecureState in |- *. 
(* Goal: and (DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s))) *)
BreakSS. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
unfold DACSecureState in |- *. 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g0 : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata p g (UsersReaders y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupReaders y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupReaders y1)) else GroupReaders y1) (UsersWriters y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupWriters y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupWriters y1)) else GroupWriters y1) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y1) (UsersOwners y1))) (GroupOwners y1)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g0)) (@set_In GRPNAME g0 (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g0 : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata p g (UsersReaders y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupReaders y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupReaders y1)) else GroupReaders y1) (UsersWriters y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupWriters y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupWriters y1)) else GroupWriters y1) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y1) (UsersOwners y1))) (GroupOwners y1)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g0)) (@set_In GRPNAME g0 (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
simpl in |- *. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
elim (OBJeq_dec o o0). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
rewrite <- a. 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o) | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
cut (fsecmat (secmat s) o = None). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o) | None => True end *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
rewrite H6. 
(* Goal: True *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
eauto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
unfold fsecmat in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
cut
 (match fsecmat (secmat s) o0 with
  | Some y => set_In u0 (ActReaders y) -> PreDACRead s u0 o0
  | None => True
  end /\
  match fsecmat (secmat s) o0 with
  | Some y => set_In u0 (ActWriters y) -> PreDACWrite s u0 o0
  | None => True
  end). 
(* Goal: forall _ : and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end, match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
elim (fsecmat (secmat s) o0). 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead s u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite s u0 o0)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0 o0) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
unfold PreDACRead, PreDACWrite, chown_acl in |- *. 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g0 : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata p g (UsersReaders y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupReaders y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupReaders y1)) else GroupReaders y1) (UsersWriters y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupWriters y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupWriters y1)) else GroupWriters y1) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y1) (UsersOwners y1))) (GroupOwners y1)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g0)) (@set_In GRPNAME g0 (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g0 : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata p g (UsersReaders y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupReaders y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupReaders y1)) else GroupReaders y1) (UsersWriters y1) (if @set_In_dec GRPNAME GRPeq_dec (group y1) (GroupWriters y1) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y1) (GroupWriters y1)) else GroupWriters y1) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y1) (UsersOwners y1))) (GroupOwners y1)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g0)) (@set_In GRPNAME g0 (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
simpl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
replace
 (facl
    (set_add ACLeq_dec
       (o,
       acldata p g (UsersReaders a)
         match set_In_dec GRPeq_dec (group a) (GroupReaders a) with
         | left _ =>
             set_add GRPeq_dec g
               (set_remove GRPeq_dec (group a) (GroupReaders a))
         | right _ => GroupReaders a
         end (UsersWriters a)
         match set_In_dec GRPeq_dec (group a) (GroupWriters a) with
         | left _ =>
             set_add GRPeq_dec g
               (set_remove GRPeq_dec (group a) (GroupWriters a))
         | right _ => GroupWriters a
         end
         (set_add SUBeq_dec p
            (set_remove SUBeq_dec (owner a) (UsersOwners a))) 
         (GroupOwners a)) (set_remove ACLeq_dec (o, a) (acl s))) o0) with
 (facl (acl s) o0). 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata p g (UsersReaders a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupReaders a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupReaders a)) else GroupReaders a) (UsersWriters a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupWriters a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupWriters a)) else GroupWriters a) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner a) (UsersOwners a))) (GroupOwners a))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
elim (facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata p g (UsersReaders a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupReaders a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupReaders a)) else GroupReaders a) (UsersWriters a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupWriters a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupWriters a)) else GroupWriters a) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner a) (UsersOwners a))) (GroupOwners a))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
unfold facl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
apply ReadWriteImpRead. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) *)
apply ReadWriteImpWrite. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChownPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s Chown t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s Chown t), StarProperty t *)
StartPSP. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H; auto. 
Qed. 
 
 
Lemma ChownPCP : forall s t : SFSstate, PreservesControlProp s Chown t. 
intros; unfold PreservesControlProp in |- *; intros Sub TF; inversion TF;
 unfold ControlProperty in |- *. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H6. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H8. 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); intro. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite <- a; auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H10 in H9; inversion H9; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (chown_acl s o p g) o0 = facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H10; rewrite H10 in H8; rewrite H7 in H8; injection H8; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (chown_acl s o p g) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold chown_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall a : AccessCtrlListData, @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata p g (UsersReaders a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupReaders a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupReaders a)) else GroupReaders a) (UsersWriters a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupWriters a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupWriters a)) else GroupWriters a) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner a) (UsersOwners a))) (GroupOwners a))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; unfold facl in |- *; apply AddRemEq. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H8. 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); intro. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite <- a; auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H10 in H9; inversion H9; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (chown_acl s o p g) o0 = facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H10; rewrite H10 in H8; rewrite H7 in H8; injection H8; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (chown_acl s o p g) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold chown_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata p g (UsersReaders y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupReaders y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupReaders y0)) else GroupReaders y0) (UsersWriters y0) (if @set_In_dec GRPNAME GRPeq_dec (group y0) (GroupWriters y0) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group y0) (GroupWriters y0)) else GroupWriters y0) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner y0) (UsersOwners y0))) (GroupOwners y0)) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall a : AccessCtrlListData, @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata p g (UsersReaders a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupReaders a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupReaders a)) else GroupReaders a) (UsersWriters a) (if @set_In_dec GRPNAME GRPeq_dec (group a) (GroupWriters a) then @set_add GRPNAME GRPeq_dec g (@set_remove GRPNAME GRPeq_dec (group a) (GroupWriters a)) else GroupWriters a) (@set_add SUBJECT SUBeq_dec p (@set_remove SUBJECT SUBeq_dec (owner a) (UsersOwners a))) (GroupOwners a))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; unfold facl in |- *; apply AddRemEq. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
intro;
 absurd
  (MACObjCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (chown_acl s o p g) (secmat s) (files s) (directories s)) o0); 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
intros;
 absurd
  (MACSubCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (chown_acl s o p g) (secmat s) (files s) (directories s)) u0); 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl s o p g) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
Qed. 
 
 
End chownIsSecure. 
 
Hint Resolve ChownPSS ChownPSP ChownPCP. 
 