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 |
|
|
14 |
definition sec :: "name \<Rightarrow> level" where
|
|
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
|
|
23 |
"sec_bexp (B bv) = 0" |
|
|
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
|