1section "Security Type Systems" 2 3subsection "Security Levels and Expressions" 4 5theory Sec_Type_Expr imports Big_Step 6begin 7 8type_synonym level = nat 9 10class sec = 11fixes sec :: "'a \<Rightarrow> nat" 12 13text\<open>The security/confidentiality level of each variable is globally fixed 14for simplicity. For the sake of examples --- the general theory does not rely 15on it! --- a variable of length \<open>n\<close> has security level \<open>n\<close>:\<close> 16 17instantiation list :: (type)sec 18begin 19 20definition "sec(x :: 'a list) = length x" 21 22instance .. 23 24end 25 26instantiation aexp :: sec 27begin 28 29fun sec_aexp :: "aexp \<Rightarrow> level" where 30"sec (N n) = 0" | 31"sec (V x) = sec x" | 32"sec (Plus a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)" 33 34instance .. 35 36end 37 38instantiation bexp :: sec 39begin 40 41fun sec_bexp :: "bexp \<Rightarrow> level" where 42"sec (Bc v) = 0" | 43"sec (Not b) = sec b" | 44"sec (And b\<^sub>1 b\<^sub>2) = max (sec b\<^sub>1) (sec b\<^sub>2)" | 45"sec (Less a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)" 46 47instance .. 48 49end 50 51 52abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool" 53 ("(_ = _ '(\<le> _'))" [51,51,0] 50) where 54"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)" 55 56abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool" 57 ("(_ = _ '(< _'))" [51,51,0] 50) where 58"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)" 59 60lemma aval_eq_if_eq_le: 61 "\<lbrakk> s\<^sub>1 = s\<^sub>2 (\<le> l); sec a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^sub>1 = aval a s\<^sub>2" 62by (induct a) auto 63 64lemma bval_eq_if_eq_le: 65 "\<lbrakk> s\<^sub>1 = s\<^sub>2 (\<le> l); sec b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^sub>1 = bval b s\<^sub>2" 66by (induct b) (auto simp add: aval_eq_if_eq_le) 67 68end 69