theory rc_theory

imports Main my_list_prefix

begin

(****************** rc policy (role, type, ... ) type definitions *****************)

(*** normal: user-defined values for policy ***)

(*** others: RC special values for RC internal control ***)

datatype t_client = 

  Client1

| Client2

datatype t_normal_role =  

  WebServer 

| WS     "t_client" 

| UpLoad "t_client" 

| CGI     "t_client"

datatype t_role = 

  InheritParentRole 

| UseForcedRole 

| InheritUpMixed 

| InheritUserRole 

| InheritProcessRole 

| NormalRole "t_normal_role" 

datatype t_normal_file_type = 

  Root_file_type   (* special value, as 0 for root-file in the NordSec paper*)

| WebServerLog_file

| WebData_file      "t_client" 

| CGI_P_file        "t_client" 

| PrivateD_file     "t_client" 

| Executable_file   (* basic protection of RC *)

datatype t_rc_file_type = 

  InheritParent_file_type          

| NormalFile_type t_normal_file_type

datatype t_normal_proc_type = 

  WebServer_proc

| CGI_P_proc "t_client"

datatype t_rc_proc_type =

  InheritParent_proc_type

| NormalProc_type t_normal_proc_type

| UseNewRoleType  

datatype t_normal_ipc_type = 

  WebIPC

datatype t_normal_rc_type =

  File_type t_normal_file_type

| Proc_type t_normal_proc_type

| IPC_type  t_normal_ipc_type

(******* Operating System type definitions ********)

type_synonym t_process = nat

type_synonym t_user = nat

type_synonym t_fname = string

type_synonym t_file = "t_fname list" 

type_synonym t_ipc = nat

(****** Access Control related type definitions *********)

datatype t_event =

  ChangeOwner  "t_process" "t_user" 

| Clone        "t_process" "t_process"

| Execute      "t_process" "t_file" 

| CreateFile   "t_process" "t_file" 

| CreateIPC    "t_process" "t_ipc" 

| ChangeRole   "t_process" "t_normal_role"    (* A process should change to normal role, which not specified in paper! *) 

(* below are events added for tainting modelling *)

| ReadFile     "t_process" "t_file" 

| WriteFile    "t_process" "t_file"     

| Send         "t_process" "t_ipc"

| Recv         "t_process" "t_ipc"

| Kill         "t_process" "t_process"

| DeleteFile   "t_process" "t_file"

| DeleteIPC    "t_process" "t_ipc"

type_synonym t_state = "t_event list"

datatype t_access_type =        (*changed by wch, original: "types access_type = nat" *)

  READ    

| WRITE   

| EXECUTE 

| CHANGE_OWNER

| CREATE

| SEND

| RECEIVE

| DELETE

(****** Some global functions' definition *****)

fun parent :: "'a list \<Rightarrow> ('a list) option"

where

   "parent []     = None"

 | "parent (n#ns) = Some ns"

definition some_in_set :: "'a set \<Rightarrow> 'a"

where

  "some_in_set S \<equiv> SOME x. x \<in> S"

lemma nonempty_set_has_ele: "S \<noteq> {} \<Longrightarrow> \<exists> e. e \<in> S" by auto

lemma some_in_set_prop: "S \<noteq> {} \<Longrightarrow> some_in_set S \<in> S"

by (drule nonempty_set_has_ele, auto simp:some_in_set_def intro:someI)

(*********** locale for RC+OS definitions **********)

definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"

where

  "bidirect_in_init S f \<equiv>  (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and> 

                           (\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)" 

locale init =

  fixes 

      init_files :: "t_file set"

  and init_file_type :: "t_file \<rightharpoonup> t_normal_file_type"

  and init_initialrole :: "t_file \<rightharpoonup> t_role"

  and init_forcedrole :: "t_file \<rightharpoonup> t_role"

  and init_processes :: "t_process set "

  and init_process_type :: "t_process \<rightharpoonup> t_normal_proc_type"

  and init_currentrole :: "t_process \<rightharpoonup> t_normal_role"

  and init_proc_forcedrole:: "t_process \<rightharpoonup> t_role"

  and init_ipcs :: "t_ipc set"

  and init_ipc_type:: "t_ipc \<rightharpoonup> t_normal_ipc_type"

  and init_users :: "t_user set"

  and init_owner :: "t_process \<rightharpoonup> t_user"

  and defrole :: "t_user \<rightharpoonup> t_normal_role" (* defrole should return normalrole, which is not

specified in NordSec paper *) 

  and default_fd_create_type :: "t_normal_role \<Rightarrow> t_rc_file_type" (* this func should only

return type for normal role, for RC special role, error ! NordSec paper*)

  and default_ipc_create_type :: "t_normal_role \<Rightarrow> t_normal_ipc_type" (* like above, NordSec paper

does not specify the domain is normal roles *)

  and default_process_create_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"

  and default_process_execute_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"

  and default_process_chown_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"

  and comproles :: "t_normal_role \<Rightarrow> t_normal_role set" (* NordSec paper do not specify all roles

here are normal *)

  and compatible :: "(t_normal_role \<times> t_normal_rc_type \<times> t_access_type) set"  (* NordSec paper do not specify all roles and all types here are normal ! *)

  assumes

      parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"

  and root_in_filesystem:  "[] \<in> init_files"

  and init_irole_has_file: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> f \<in> init_files"

  and init_frole_has_file: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> f \<in> init_files"

  and init_ftype_has_file: "\<And> f t. init_file_type f = Some t \<Longrightarrow> f \<in> init_files"

  and

      init_proc_has_role:  "bidirect_in_init init_processes init_currentrole"

  and init_proc_has_frole: "bidirect_in_init init_processes init_proc_forcedrole"

  and init_proc_has_type:  "bidirect_in_init init_processes init_process_type"

  and

      init_ipc_has_type:   "bidirect_in_init init_ipcs init_ipc_type"

  and

      init_user_has_role:  "bidirect_in_init init_users defrole"

  and init_proc_has_owner: "bidirect_in_init init_processes init_owner"

  and init_owner_valid:    "\<And> p u. init_owner p = Some u \<Longrightarrow> u \<in> init_users"

  and

      init_finite: "finite init_files \<and> finite init_processes \<and> finite init_ipcs \<and> finite init_users"

begin 

(***** Operating System Listeners *****)

fun current_files :: "t_state \<Rightarrow> t_file set"

where

  "current_files [] = init_files"

| "current_files (CreateFile p f # s) = insert f (current_files s)"

| "current_files (DeleteFile p f # s) = current_files s - {f}"

| "current_files (_ # s) = current_files s"

fun current_procs :: "t_state \<Rightarrow> t_process set"

where

  "current_procs [] = init_processes"

| "current_procs (Clone p p' # s) = insert p' (current_procs s)"

| "current_procs (Kill p p' # s) = current_procs s - {p'} "

| "current_procs (_ # s) = current_procs s"

fun current_ipcs :: "t_state \<Rightarrow> t_ipc set"

where

  "current_ipcs [] = init_ipcs" 

| "current_ipcs (CreateIPC p i # s) = insert i (current_ipcs s)"

| "current_ipcs (DeleteIPC p i # s) = current_ipcs s - {i}"

| "current_ipcs (_ # s) = current_ipcs s"

fun owner :: "t_state \<Rightarrow> t_process \<rightharpoonup> t_user"

where

  "owner [] = init_owner"

| "owner (Clone p p' # \<tau>) = (owner \<tau>) (p' := owner \<tau> p)"

| "owner (ChangeOwner p u # \<tau>) = (owner \<tau>) (p := Some u)"

| "owner (_ # \<tau>) = owner \<tau>"

(***** functions for rc internal *****)

(*** Roles Functions ***)

(* comments:

We have fix init_initialrole already in locale, why need this function?

 Cause, users may be lazy to specify every file in the initial state to some InheritParent as

initialrole, they can just specify all the important files with special initial role, leaving

all other None, it is init_file_initialrole's job to fill default value(InheritParent) for 

other files. Accutally, this has the point of "Functional default settings" in the 2 section of

the NordSec paper. 

init_file_forcedrole, and init_file_type_aux are of the same meaning. 

*)

fun init_file_initialrole :: "t_file \<rightharpoonup> t_role"

where

  "init_file_initialrole [] = (case (init_initialrole []) of

                            None   \<Rightarrow> Some UseForcedRole

                          | Some r \<Rightarrow> Some r)"

| "init_file_initialrole f  = (case (init_initialrole f) of

                            None   \<Rightarrow> Some InheritParentRole

                          | Some r \<Rightarrow> Some r)"

fun initialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"  

where

  "initialrole [] = init_file_initialrole"

| "initialrole (CreateFile p f # s) = (initialrole s) (f:= Some InheritParentRole)" 

| "initialrole (_ # s) = initialrole s"

fun erole_functor :: "(t_file \<rightharpoonup> t_role) \<Rightarrow> t_role \<Rightarrow> (t_file \<rightharpoonup> t_role)"

where

  "erole_functor rfunc r [] = (

     if (rfunc [] = Some InheritParentRole) 

     then Some r 

     else rfunc [] )"                             

| "erole_functor rfunc r (n#ns) = (

     if (rfunc (n#ns) = Some InheritParentRole) 

     then erole_functor rfunc r ns 

     else rfunc (n#ns) )"

definition effinitialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"

where

  "effinitialrole s \<equiv> erole_functor (initialrole s) UseForcedRole"

fun init_file_forcedrole :: "t_file \<rightharpoonup> t_role"

where

  "init_file_forcedrole [] = ( case (init_forcedrole []) of

                                 None   \<Rightarrow> Some InheritUpMixed

                               | Some r \<Rightarrow> Some r )"

| "init_file_forcedrole f  = ( case (init_forcedrole f) of 

                                 None   \<Rightarrow> Some InheritParentRole

                              |  Some r \<Rightarrow> Some r )"  

fun forcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"  

where

  "forcedrole [] = init_file_forcedrole"

| "forcedrole (CreateFile p f # s) = (forcedrole s) (f:= Some InheritParentRole)" 

| "forcedrole (_ # s) = forcedrole s" 

definition effforcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" 

where

  "effforcedrole s \<equiv> erole_functor (forcedrole s) InheritUpMixed"

fun proc_forcedrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_role)" (* $6.7$ *) 

where

  "proc_forcedrole [] = init_proc_forcedrole"

| "proc_forcedrole (Execute p f # s) = (proc_forcedrole s) (p := effforcedrole s f)"    

| "proc_forcedrole (Clone p p' # s) = (proc_forcedrole s) (p' := proc_forcedrole s p)" 

| "proc_forcedrole (e # s) = proc_forcedrole s"

fun currentrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_role)" 

where 

  "currentrole [] = init_currentrole"

| "currentrole (Clone p p' # \<tau>) = (currentrole \<tau>) (p' := currentrole \<tau> p)" 

| "currentrole (Execute p f # \<tau>) = (currentrole \<tau>) (p := 

     case (effinitialrole \<tau> f) of 

       Some ir \<Rightarrow> (case ir of 

                     NormalRole r \<Rightarrow> Some r

                   | UseForcedRole \<Rightarrow> (

                       case (effforcedrole \<tau> f) of

                         Some fr \<Rightarrow> (case fr of

                                       NormalRole r \<Rightarrow> Some r

                                     | InheritUserRole \<Rightarrow> (defrole \<circ>\<^sub>m (owner \<tau>)) p

                                     | InheritProcessRole \<Rightarrow> currentrole \<tau> p

                                     | InheritUpMixed \<Rightarrow> currentrole \<tau> p

                                     | _ \<Rightarrow> None )

                       | _ \<Rightarrow> None    )

                   | _  \<Rightarrow> None )

     | _ \<Rightarrow> None                                   )"       

| "currentrole (ChangeOwner p u # \<tau>) = (currentrole \<tau>) (p := 

     case (proc_forcedrole \<tau> p) of 

       Some fr \<Rightarrow> (case fr of

                     NormalRole r \<Rightarrow> Some r

                   | InheritProcessRole \<Rightarrow> currentrole \<tau> p

                   | InheritUserRole \<Rightarrow> defrole u

                   | InheritUpMixed \<Rightarrow> defrole u

                   | _ \<Rightarrow> None)

     | _ \<Rightarrow> None                                       )"  

| "currentrole (ChangeRole p r # \<tau>) = (currentrole \<tau>) (p := Some r)"

| "currentrole (_ # \<tau>) = currentrole \<tau>"  

(*** Types Functions ***)

fun init_file_type_aux :: "t_file \<rightharpoonup> t_rc_file_type"

where

  "init_file_type_aux f = (if (f \<in> init_files)

                         then (case (init_file_type f) of 

                                 Some t \<Rightarrow> Some (NormalFile_type t)

                               | _      \<Rightarrow> Some InheritParent_file_type)

                         else None)"

fun type_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_rc_file_type)" (* (6) *)

where

  "type_of_file [] = init_file_type_aux" 

| "type_of_file (CreateFile p f # s) = (

     case (currentrole s p) of

       Some r \<Rightarrow> (type_of_file s) (f := Some (default_fd_create_type r))

     | _      \<Rightarrow> (type_of_file s) (f := None))" 

| "type_of_file (_ # s) = type_of_file s"  (* add by wch *)

fun etype_aux:: "(t_file \<rightharpoonup> t_rc_file_type) \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)"

where

  "etype_aux typf [] = (

     case (typf []) of 

       Some InheritParent_file_type \<Rightarrow> Some Root_file_type

     | Some (NormalFile_type t) \<Rightarrow> Some t

     | None \<Rightarrow> None )"        

| "etype_aux typf (n#ns) = (

     case (typf (n#ns)) of

       Some InheritParent_file_type \<Rightarrow> etype_aux typf ns

     | Some (NormalFile_type t) \<Rightarrow> Some t

     | None \<Rightarrow> None )"  

definition etype_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)" 

    (* etype is always normal *)

where

  "etype_of_file s \<equiv> etype_aux (type_of_file s)"              

definition pct :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"

where

  "pct s p \<equiv> (case (currentrole s p) of

                Some r \<Rightarrow> Some (default_process_create_type r)

              | _      \<Rightarrow> None)"

definition pet :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"

where

  "pet s p \<equiv> (case (currentrole s p) of

                Some r \<Rightarrow> Some (default_process_execute_type r)

              | _      \<Rightarrow> None)"

definition pot :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"

where

  "pot s p \<equiv> (case (currentrole s p) of

                Some r \<Rightarrow> Some (default_process_chown_type r)

              | _      \<Rightarrow> None)"

fun type_of_process :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_proc_type)" 

where

  "type_of_process [] = init_process_type"

| "type_of_process (Clone p p' # \<tau>) = (type_of_process \<tau>) (p' := 

     case (pct \<tau> p) of

       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p

     | Some (NormalProc_type tp)    \<Rightarrow> Some tp

     | _                            \<Rightarrow> None               )" (*6.80*)

| "type_of_process (Execute p f # \<tau>) = (type_of_process \<tau>) (p :=

     case (pet \<tau> p) of

       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p

     | Some (NormalProc_type tp)    \<Rightarrow> Some tp

     | _                            \<Rightarrow> None                )" (*6.82*)

| "type_of_process (ChangeOwner p u # \<tau>) = (type_of_process \<tau>) (p :=

     case (pot \<tau> p) of

       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p

     | Some UseNewRoleType          \<Rightarrow> (case (pct (ChangeOwner p u # \<tau>) p) of 

                                          Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p

                                        | Some (NormalProc_type tp)    \<Rightarrow> Some tp

                                        | _                            \<Rightarrow> None)

     | Some (NormalProc_type tp)    \<Rightarrow> Some tp

     | _                            \<Rightarrow> None                    )"   (* the UseNewRoleType case is refered with Nordsec paper 4 (11), and it is not right??! of just

use "pct" *)

| "type_of_process (_ # \<tau>) = type_of_process \<tau>" 

fun type_of_ipc :: "t_state \<Rightarrow> (t_ipc \<rightharpoonup> t_normal_ipc_type)" (* (14) *)

where

  "type_of_ipc [] = init_ipc_type" 

| "type_of_ipc (CreateIPC p i # s) = (type_of_ipc s) (i := 

     case (currentrole s p) of

       Some r \<Rightarrow> Some (default_ipc_create_type r)

     | _      \<Rightarrow> None                                )"

| "type_of_ipc (_ # s) = type_of_ipc s" (* add by wch *)

(*** RC access control ***)

fun rc_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"

where

  "rc_grant \<tau> (CreateFile p f) = (

     case (parent f) of

       Some pf \<Rightarrow> (

         case (currentrole \<tau> p, etype_of_file \<tau> pf) of

           (Some r, Some t) \<Rightarrow> (

              case (default_fd_create_type r) of

                InheritParent_file_type \<Rightarrow> (r, File_type t, WRITE) \<in> compatible 

              | NormalFile_type t' \<Rightarrow> (r, File_type t, WRITE) \<in> compatible \<and> (r, File_type t', CREATE) \<in> compatible

                               )

         | _               \<Rightarrow> False )

     | _       \<Rightarrow> False                         )"  

| "rc_grant \<tau> (ReadFile p f) = (

     case (currentrole \<tau> p, etype_of_file \<tau> f) of

        (Some r, Some t) \<Rightarrow> (r, File_type t, READ) \<in> compatible 

     | _                \<Rightarrow> False                )"

| "rc_grant \<tau> (WriteFile p f) = (

     case (currentrole \<tau> p, etype_of_file \<tau> f) of

       (Some r, Some t) \<Rightarrow> (r, File_type t, WRITE) \<in> compatible 

     | _      \<Rightarrow> False                          )"

| "rc_grant \<tau> (Execute p f) = (

     case (currentrole \<tau> p, etype_of_file \<tau> f) of

       (Some r, Some t) \<Rightarrow> (r, File_type t, EXECUTE) \<in> compatible

     | _                \<Rightarrow> False               )"     

| "rc_grant \<tau> (ChangeOwner p u) = (

     case (currentrole \<tau> p, type_of_process \<tau> p) of

       (Some r, Some t) \<Rightarrow> (r, Proc_type t, CHANGE_OWNER) \<in> compatible

     | _      \<Rightarrow> False                         )" 

| "rc_grant \<tau> (Clone p newproc) = (

     case (currentrole \<tau> p, type_of_process \<tau> p) of

       (Some r, Some t) \<Rightarrow> (r, Proc_type t, CREATE) \<in> compatible

     | _      \<Rightarrow> False                         )" (* premiss of no limit to clone is removed to locale assumptions *)

| "rc_grant \<tau> (ChangeRole p r) = (

     case (currentrole \<tau> p) of

       Some cr \<Rightarrow> r \<in> comproles cr

     | _       \<Rightarrow> False                        )"

| "rc_grant \<tau> (Send p i) = (

     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 

       (Some r, Some t) \<Rightarrow> (r, IPC_type t, SEND) \<in> compatible

     | _                \<Rightarrow> False               )"

| "rc_grant \<tau> (Recv p i) = (

     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 

       (Some r, Some t) \<Rightarrow> (r, IPC_type t, RECEIVE) \<in> compatible

     | _                \<Rightarrow> False               )"

| "rc_grant \<tau> (CreateIPC p i) = (

     case (currentrole \<tau> p) of

       Some r \<Rightarrow> (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible

     | _      \<Rightarrow> False                         )"

| "rc_grant \<tau> (DeleteFile p f) = (

     case (currentrole \<tau> p, etype_of_file \<tau> f) of 

       (Some r, Some t) \<Rightarrow> (r, File_type t, DELETE) \<in> compatible

     | _                \<Rightarrow> False               )"

| "rc_grant \<tau> (DeleteIPC p i) = (

     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 

       (Some r, Some t) \<Rightarrow> (r, IPC_type t, DELETE) \<in> compatible

     | _                \<Rightarrow> False               )"

| "rc_grant \<tau> (Kill p p') = (

     case (currentrole \<tau> p, type_of_process \<tau> p') of 

       (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible

     | _                \<Rightarrow> False               )"

(* new file pathname is user-defined, so os just check if its unexistence *) 

fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"

where

  "os_grant \<tau> (Execute p f)    = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"

| "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))"  (*cannot create disk, ?? or f = [] ??*)

| "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)"

| "os_grant \<tau> (ReadFile p f)   = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"

| "os_grant \<tau> (WriteFile p f)  = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"

| "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"

| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *)

| "os_grant \<tau> (Send p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 

| "os_grant \<tau> (Recv p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"

| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *)

| "os_grant \<tau> (Kill p p')      = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" 

| "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"

| "os_grant \<tau> (DeleteIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 

(**** system valid state ****)

inductive valid :: "t_state \<Rightarrow> bool"

where

  vs_nil:  "valid []"

| vs_step: "\<lbrakk>valid s; os_grant s e; rc_grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"

end

(*** more RC constrains of type system in formalisation ***)

locale rc_basic = init +

  assumes 

      init_initialrole_valid: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"   (* 6.10 *)

  and init_forcedrole_valid:  "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.11 *)

  and init_proc_forcedrole_valid: "\<And> p r. init_proc_forcedrole p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.7 *)

  and default_fd_create_type_valid: "\<And> nr t. default_fd_create_type nr = t \<Longrightarrow> t = InheritParent_file_type \<or> (\<exists> nt. t = NormalFile_type nt)" (*6.16*)

  and default_process_create_type_valid: "\<And> nr t. default_process_create_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.18*)

  and default_process_chown_type_valid: "\<And> nr t. default_process_chown_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.19*)

  and default_process_execute_type_valid: "\<And> nr t. default_process_execute_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.20*)

begin

lemma init_file_initialrole_valid: "init_file_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"

apply (induct f)

by (auto simp:init_file_initialrole.simps dest:init_initialrole_valid split:option.splits)

lemma initialrole_valid: "initialrole \<tau> f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"   (* 6.10 *)

apply (induct \<tau> arbitrary:f)  defer

apply (case_tac a)

apply (auto simp:initialrole.simps dest:init_file_initialrole_valid 

            split:option.splits if_splits)

done

lemma effinitialrole_valid: "effinitialrole \<tau> f = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" 

apply (induct f)

apply (auto simp:effinitialrole_def dest:initialrole_valid split:option.splits if_splits)

done

lemma init_file_forcedrole_valid: 

  "init_file_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" 

apply (induct f)

by (auto simp:init_file_forcedrole.simps dest:init_forcedrole_valid split:option.splits)

lemma forcedrole_valid: "forcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.10 *)

apply (induct \<tau> arbitrary:f) defer