43158

1 
header "Security Type Systems"


2 


3 
theory Sec_Type_Expr imports Big_Step


4 
begin


5 


6 
subsection "Security Levels and Expressions"


7 


8 
type_synonym level = nat


9 


10 
text{* The security/confidentiality level of each variable is globally fixed


11 
for simplicity. For the sake of examples  the general theory does not rely


12 
on it!  a variable of length @{text n} has security level @{text n}: *}


13 

45212

14 
definition sec :: "vname \<Rightarrow> level" where

43158

15 
"sec n = size n"


16 


17 
fun sec_aexp :: "aexp \<Rightarrow> level" where


18 
"sec_aexp (N n) = 0" 


19 
"sec_aexp (V x) = sec x" 


20 
"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"


21 


22 
fun sec_bexp :: "bexp \<Rightarrow> level" where

45200

23 
"sec_bexp (Bc v) = 0" 

43158

24 
"sec_bexp (Not b) = sec_bexp b" 


25 
"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" 


26 
"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"


27 


28 


29 
abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"


30 
("(_ = _ '(\<le> _'))" [51,51,0] 50) where


31 
"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)"


32 


33 
abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"


34 
("(_ = _ '(< _'))" [51,51,0] 50) where


35 
"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"


36 


37 
lemma aval_eq_if_eq_le:


38 
"\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l); sec_aexp a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"


39 
by (induct a) auto


40 


41 
lemma bval_eq_if_eq_le:


42 
"\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l); sec_bexp b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"


43 
by (induct b) (auto simp add: aval_eq_if_eq_le)


44 


45 
end
