Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section chsubscIsSecure. 
 
Lemma ChsubscPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre7 s -> SecureState s -> TransFunc u s Chsubsc t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre7 s) (_ : SecureState s) (_ : TransFunc u s Chsubsc t), SecureState t *)
intros s t Sub FP7 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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) *)
unfold SecureState in |- *. 
(* Goal: and (DACSecureState (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s))) *)
BreakSS. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) *)
unfold MACSecureState in |- *; simpl in |- *. 
(* Goal: forall (u0 : SUBJECT) (o : OBJECT), match fsecmat (secmat s) o with | Some x => match fOSC (objectSC s) o with | Some y => match fSSC (chsubsc_SC s u sc) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intros; elim (SUBeq_dec u u0); intro y0. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (objectSC s) o with | Some y => match fSSC (chsubsc_SC s u sc) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (objectSC s) o with | Some y => match fSSC (chsubsc_SC s u sc) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite <- y0. 
elim (fsecmat (secmat s) o); elim (fSSC (chsubsc_SC s u sc) u);
 elim (fOSC (objectSC s) o); (intros; contradiction || auto). 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
absurd (set_In u (ActReaders a1) \/ set_In u (ActWriters a1)); auto. 
 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (objectSC s) o with | Some y => match fSSC (chsubsc_SC s u sc) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fSSC (chsubsc_SC s u sc) u0) with (fSSC (subjectSC s) u0). 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold MACSecureState in MAC; apply MAC; auto. 
 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChsubscPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s Chsubsc t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s Chsubsc t), StarProperty t *)
StartPSP. 
(* 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: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChsubscPCP : forall s t : SFSstate, PreservesControlProp s Chsubsc 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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) o, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
intro;
 absurd
  (DACCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (acl s) (secmat s) (files s) (directories s)) o); 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (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) (chsubsc_SC s u sc) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (acl s) (secmat s) (files s) (directories s)) o); 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (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) (chsubsc_SC s u sc) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
End chsubscIsSecure. 
 
Hint Resolve ChsubscPSS ChsubscPSP ChsubscPCP. 
 