Require Export ModelProperties. 
Require Export aclstatIsSecure. 
Require Export chmodIsSecure. 
Require Export createIsSecure. 
Require Export mkdirIsSecure. 
Require Export openIsSecure. 
Require Export addUsrGrpToAclIsSecure. 
Require Export chobjscIsSecure. 
Require Export chownIsSecure. 
Require Export chsubscIsSecure. 
Require Export closeIsSecure. 
Require Export delUsrGrpFromAclIsSecure. 
Require Export oscstatIsSecure. 
Require Export owner_closeIsSecure. 
Require Export readIsSecure. 
Require Export readdirIsSecure. 
Require Export rmdirIsSecure. 
Require Export sscstatIsSecure. 
Require Export statIsSecure. 
Require Export unlinkIsSecure. 
Require Export writeIsSecure. 
Require Import InitialState. 
Require Export Le. 
 
 
(*This definition generalizes the notion of secure state. It includes*) 
(*all the security relevant conditions and also the mathematicals    *) 
(*ones (for instance the one that asserts that subjectSC is a partial*) 
(*function).                                                         *) 
 
Definition GeneralSecureState (s : SFSstate) : Prop :=
  SecureState s /\
  StarProperty s /\
  FuncPre1 s /\
  FuncPre2 s /\
  FuncPre3 s /\ FuncPre4 s /\ FuncPre5 s /\ FuncPre6 s /\ FuncPre7 s. 
 
(*********************************************************************) 
(*                       The Model's Lemmas                          *) 
(*********************************************************************) 
 
 
(*The following Lemma shows that the initial state is a secure state.*) 
 
Lemma InitialStateIsSecure : GeneralSecureState InitState. 
unfold GeneralSecureState, SecureState, InitState, DACSecureState,
 MACSecureState, StarProperty, FuncPre1, FuncPre2, FuncPre3, FuncPre4,
 FuncPre5, FuncPre6, FuncPre7 in |- *; simpl in |- *. 
(* Goal: and (and (forall (_ : SUBJECT) (_ : OBJECT), True) (forall (_ : SUBJECT) (_ : OBJECT), True)) (and (forall (_ : SUBJECT) (_ : OBJECT) (_ : OBJECT), True) (and (and (forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@nil OBJECT) (@nil OBJECT)))) (and (@eq (set OBJECT) (@nil OBJECT) (@nil OBJECT)) (and (@Included OBJECT (@nil OBJECT) (@nil OBJECT)) (and True (and True (and True (@IsPARTFUNC SUBJECT SecClass SUBeq_dec SysSubjectSC)))))))) *)
repeat (split; auto). 
(* Goal: forall (groups : forall _ : GRPNAME, set SUBJECT) (primaryGrp : forall _ : SUBJECT, GRPNAME) (subjectSC : set (prod SUBJECT SecClass)) (AllGrp RootGrp SecAdmGrp : GRPNAME) (objectSC : set (prod OBJECT SecClass)) (acl : set (prod OBJECT AccessCtrlListData)) (secmat : set (prod OBJECT ReadersWriters)) (files : set (prod OBJECT FILECONT)) (directories : set (prod OBJECT DIRCONT)) (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
intros.
(* Goal: @eq OBJTYPE (ObjType o) Directory *)
(* Goal: forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) File *)
elim (fSSC SysSubjectSC root); auto. 
 
(* Goal: forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) File *)
contradiction. 
 
(* Goal: forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) File *)
contradiction. 

(* Goal: forall (o : OBJECT) (_ : False), @eq OBJTYPE (ObjType o) File *)
contradiction.
 
Qed. 

 
(*The main lemma deals with secuences of SFSstates.                  *) 
(*In that lemma we'll use the function nth (defined in PolyList)     *) 
(*which takes a natural (n), a list, and a default element with the  *) 
(*type of the list, and returns the n(th) element of list if there   *) 
(*are enough elements in it, or the default element if not.          *) 
(*For this reason, we need to define a default SFSstate. In fact we  *) 
(*won't use it in the proof, it's just a type requirement.           *) 
 
Parameter defaultState : SFSstate. 
 
 
(*The main Lemma for the model is the following one, wich says that  *) 
(*for any given sequence of states such that the initial state is    *) 
(*secure and for any two consecutives states, s and t, exists an     *) 
(*operation (op) and a user (u) executing it, such that              *) 
(*(TransFunc u s op t) holds, then every state in the secuence is    *) 
(*secure.                                                            *) 
 
Lemma BasicSecurityTheorem :
 forall tr : list SFSstate,
 GeneralSecureState (nth 0 tr defaultState) ->
 (forall n : nat,
  n < length tr ->
  exists op : Operation,
    (exists u : SUBJECT,
       TransFunc u (nth n tr defaultState) op (nth (S n) tr defaultState))) ->
 forall n : nat, n <= length tr -> GeneralSecureState (nth n tr defaultState). 
(* Goal: forall (groups : forall _ : GRPNAME, set SUBJECT) (primaryGrp : forall _ : SUBJECT, GRPNAME) (subjectSC : set (prod SUBJECT SecClass)) (AllGrp RootGrp SecAdmGrp : GRPNAME) (objectSC : set (prod OBJECT SecClass)) (acl : set (prod OBJECT AccessCtrlListData)) (secmat : set (prod OBJECT ReadersWriters)) (files : set (prod OBJECT FILECONT)) (directories : set (prod OBJECT DIRCONT)) (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
intros. 
induction  n as [| n Hrecn]. 
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
auto. 
 
(* Goal: GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
generalize Hrecn. 
cut
 (exists op : Operation,
    (exists u : SUBJECT,
       TransFunc u (nth n tr defaultState) op (nth (S n) tr defaultState))). 
(* Goal: forall (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (@nth SFSstate n tr defaultState)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
elim (nth n tr defaultState). 
(* Goal: forall (groups : forall _ : GRPNAME, set SUBJECT) (primaryGrp : forall _ : SUBJECT, GRPNAME) (subjectSC : set (prod SUBJECT SecClass)) (AllGrp RootGrp SecAdmGrp : GRPNAME) (objectSC : set (prod OBJECT SecClass)) (acl : set (prod OBJECT AccessCtrlListData)) (secmat : set (prod OBJECT ReadersWriters)) (files : set (prod OBJECT FILECONT)) (directories : set (prod OBJECT DIRCONT)) (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
intros. 
(* Goal: forall (groups : forall _ : GRPNAME, set SUBJECT) (primaryGrp : forall _ : SUBJECT, GRPNAME) (subjectSC : set (prod SUBJECT SecClass)) (AllGrp RootGrp SecAdmGrp : GRPNAME) (objectSC : set (prod OBJECT SecClass)) (acl : set (prod OBJECT AccessCtrlListData)) (secmat : set (prod OBJECT ReadersWriters)) (files : set (prod OBJECT FILECONT)) (directories : set (prod OBJECT DIRCONT)) (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
elim H2; intros. 
(* Goal: forall (groups : forall _ : GRPNAME, set SUBJECT) (primaryGrp : forall _ : SUBJECT, GRPNAME) (subjectSC : set (prod SUBJECT SecClass)) (AllGrp RootGrp SecAdmGrp : GRPNAME) (objectSC : set (prod OBJECT SecClass)) (acl : set (prod OBJECT AccessCtrlListData)) (secmat : set (prod OBJECT ReadersWriters)) (files : set (prod OBJECT FILECONT)) (directories : set (prod OBJECT DIRCONT)) (_ : @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) op (@nth SFSstate (S n) tr defaultState)))) (_ : forall _ : le n (@length SFSstate tr), GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
elim H3; intros. 
cut
 (forall u : SUBJECT,
  GeneralSecureState
    (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl
       secmat files directories) ->
  TransFunc u
    (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl
       secmat files directories) x (nth (S n) tr defaultState) ->
  GeneralSecureState (nth (S n) tr defaultState)). 
(* Goal: forall _ : forall (u : SUBJECT) (_ : GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)) (_ : TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) x (@nth SFSstate (S n) tr defaultState)), GeneralSecureState (@nth SFSstate (S n) tr defaultState), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: forall (u : SUBJECT) (_ : GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)) (_ : TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) x (@nth SFSstate (S n) tr defaultState)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
intro GTR; apply (GTR x0). 
(* Goal: GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) *)
(* Goal: TransFunc x0 (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) x (@nth SFSstate (S n) tr defaultState) *)
(* Goal: forall (u : SUBJECT) (_ : GeneralSecureState (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories)) (_ : TransFunc u (mkSFS groups primaryGrp subjectSC AllGrp RootGrp SecAdmGrp objectSC acl secmat files directories) x (@nth SFSstate (S n) tr defaultState)), GeneralSecureState (@nth SFSstate (S n) tr defaultState) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
apply Hrecn0; auto with *. 
 
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
auto. 
 
unfold GeneralSecureState in |- *; intros u GSSi TF; decompose [and] GSSi;
 clear GSSi. 
(* Goal: and (FuncPre1 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre2 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre3 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre4 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre5 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre6 (@nth SFSstate (S n) tr defaultState)) (FuncPre7 (@nth SFSstate (S n) tr defaultState))))))) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
split. 
induction  x as [| | | | | | | | | | | | | | | | | | | ];
 prolog
  [ AclstatPSS AddUsrGrpToAclPSS ChmodPSS ChobjscPSS ChownPSS ChsubscPSS
   ClosePSS CreatePSS DelUsrGrpFromAclPSS MkdirPSS OpenPSS OscstatPSS
   Owner_ClosePSS ReadPSS ReaddirPSS RmdirPSS SscstatPSS StatPSS UnlinkPSS
   WritePSS ] 2. 
 
(* Goal: and (FuncPre1 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre2 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre3 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre4 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre5 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre6 (@nth SFSstate (S n) tr defaultState)) (FuncPre7 (@nth SFSstate (S n) tr defaultState))))))) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
split. 
induction  x as [| | | | | | | | | | | | | | | | | | | ];
 prolog
  [ AclstatPSP AddUsrGrpToAclPSP ChmodPSP ChobjscPSP ChownPSP ChsubscPSP
   ClosePSP CreatePSP DelUsrGrpFromAclPSP MkdirPSP OpenPSP OscstatPSP
   Owner_ClosePSP ReadPSP ReaddirPSP RmdirPSP SscstatPSP StatPSP UnlinkPSP
   WritePSP ] 2. 
 
(* Goal: and (FuncPre1 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre2 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre3 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre4 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre5 (@nth SFSstate (S n) tr defaultState)) (and (FuncPre6 (@nth SFSstate (S n) tr defaultState)) (FuncPre7 (@nth SFSstate (S n) tr defaultState))))))) *)
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
split. 
unfold FuncPre1 in |- *; unfold FuncPre1 in H6; decompose [and] H6;
 repeat (split; eauto). 
 
unfold FuncPre2, FuncPre3, FuncPre4, FuncPre5, FuncPre6, FuncPre7 in |- *;
 unfold FuncPre2, FuncPre3, FuncPre4, FuncPre5, FuncPre6, FuncPre7
  in H8, H9, H10, H11, H12, H14; repeat (split; eauto). 
 
(* Goal: @ex Operation (fun op : Operation => @ex SUBJECT (fun u : SUBJECT => TransFunc u (@nth SFSstate n tr defaultState) op (@nth SFSstate (S n) tr defaultState))) *)
auto. 
 
Qed.