Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section readdirIsSecure. 
 
Lemma ReaddirPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 SecureState s -> TransFunc u s Readdir t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : SecureState s) (_ : TransFunc u s Readdir t), SecureState t *)
OpDontChangeStPSS. 
Qed. 
 
 
Lemma ReaddirPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s Readdir t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s Readdir t), StarProperty t *)
OpDontChangeStPSP. 
Qed. 
 
 
Lemma ReaddirPCP : forall s t : SFSstate, PreservesControlProp s Readdir t. 
intros; unfold PreservesControlProp in |- *; intros Sub TF; inversion TF;
 unfold ControlProperty in |- *. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged t t o0, ExecuterIsOwner t Sub o0) (forall _ : MACObjCtrlAttrHaveChanged t t o0, @set_In SUBJECT Sub (groups t (SecAdmGrp t))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
split. 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged t t o, ExecuterIsOwner t Sub o) (forall _ : MACObjCtrlAttrHaveChanged t t o, @set_In SUBJECT Sub (groups t (SecAdmGrp t))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
intros. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged t t o0, ExecuterIsOwner t Sub o0) (forall _ : MACObjCtrlAttrHaveChanged t t o0, @set_In SUBJECT Sub (groups t (SecAdmGrp t))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
split. 
(* Goal: forall _ : DACCtrlAttrHaveChanged t t o0, ExecuterIsOwner t Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged t t o0, @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
intro. 
(* Goal: ExecuterIsOwner t Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged t t o0, @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
absurd (DACCtrlAttrHaveChanged t t o0); auto. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged t t o0, @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
intro; absurd (MACObjCtrlAttrHaveChanged t t o0); auto. 
 
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged t t u0), @set_In SUBJECT Sub (groups t (SecAdmGrp t)) *)
intros; absurd (MACSubCtrlAttrHaveChanged t t u0); auto. 
 
Qed. 
 
 
End readdirIsSecure. 
 
Hint Resolve ReaddirPSS ReaddirPSP ReaddirPCP. 
 