Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section chobjscIsSecure. 
 
Lemma ChobjscPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre6 s -> SecureState s -> TransFunc u s Chobjsc t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre6 s) (_ : SecureState s) (_ : TransFunc u s Chobjsc t), SecureState t *)
intros s t Sub FP6 SS TF; inversion TF. 
(* 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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) *)
unfold MACSecureState in |- *; simpl in |- *; intros. 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o0). 
(* Goal: forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite <- a. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (chobjsc_SC s o sc) o with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
cut (fsecmat (secmat s) o = None). 
(* Goal: forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (chobjsc_SC s o sc) o with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | 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 x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite H6. 
elim (fOSC (objectSC s) o); elim (fOSC (chobjsc_SC s o sc) o);
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 elim (fSSC (subjectSC s) u); contradiction || auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold fsecmat in |- *; auto. 
 
(* Goal: forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (chobjsc_SC s o sc) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fOSC (chobjsc_SC s o sc) o0) with (fOSC (objectSC s) o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u with | Some z => forall _ : or (@set_In SUBJECT u (ActReaders x)) (@set_In SUBJECT u (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o0) (fOSC (chobjsc_SC s o sc) o0) *)
unfold MACSecureState in MAC; apply MAC. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChobjscPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre6 s -> StarProperty s -> TransFunc u s Chobjsc t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre6 s) (_ : StarProperty s) (_ : TransFunc u s Chobjsc t), StarProperty t *)
intros s t Sub FP6 SP TF; inversion TF. 
(* 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: StarProperty (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) *)
unfold StarProperty in |- *; simpl in |- *; intros. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o1); elim (OBJeq_dec o o2); intros EQ2 EQ1. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
rewrite <- EQ1; rewrite <- EQ2. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o with | Some x => match fOSC (chobjsc_SC s o sc) o with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
elim (fOSC (objectSC s) o); elim (fOSC (chobjsc_SC s o sc) o);
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 contradiction || auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
rewrite <- EQ1. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o with | Some x => match fOSC (chobjsc_SC s o sc) o with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fOSC (chobjsc_SC s o sc) o2) with (fOSC (objectSC s) o2). 
elim (fsecmat (secmat s) o2); elim (fOSC (chobjsc_SC s o sc) o);
 elim (fOSC (objectSC s) o); elim (fOSC (objectSC s) o2); 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 intros; contradiction || auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
rewrite <- EQ2. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o with | Some x => match fOSC (chobjsc_SC s o sc) o with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (chobjsc_SC s o sc) o2) *)
replace (fOSC (chobjsc_SC s o sc) o1) with (fOSC (objectSC s) o1). 
elim (fsecmat (secmat s) o1); elim (fOSC (chobjsc_SC s o sc) o);
 elim (fOSC (objectSC s) o); elim (fOSC (objectSC s) o1); 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 intros; contradiction || auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (chobjsc_SC s o sc) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fOSC (chobjsc_SC s o sc) o2) with (fOSC (objectSC s) o2). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (chobjsc_SC s o sc) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (chobjsc_SC s o sc) o2) *)
replace (fOSC (chobjsc_SC s o sc) o1) with (fOSC (objectSC s) o1). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (objectSC s) o1 with | Some z => forall (_ : @set_In SUBJECT u (ActWriters w)) (_ : @set_In SUBJECT u (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o1) (fOSC (chobjsc_SC s o sc) o1) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (chobjsc_SC s o sc) o2) *)
unfold StarProperty in SP; apply SP. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChobjscPCP : forall s t : SFSstate, PreservesControlProp s Chobjsc 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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
absurd
 (DACCtrlAttrHaveChanged s
    (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
       (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) 
       (acl s) (secmat s) (files s) (directories s)) o0); 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
absurd
 (MACSubCtrlAttrHaveChanged s
    (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
       (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) 
       (acl s) (secmat s) (files s) (directories s)) u0); 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (chobjsc_SC s o sc) (acl s) (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) (chobjsc_SC s o sc) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
Qed. 
 
 
End chobjscIsSecure. 
 
Hint Resolve ChobjscPSS ChobjscPSP ChobjscPCP.