author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 53015 | a1119cf551e8 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
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 |
||
50342 | 10 |
class sec = |
11 |
fixes sec :: "'a \<Rightarrow> nat" |
|
12 |
||
43158 | 13 |
text{* The security/confidentiality level of each variable is globally fixed |
14 |
for simplicity. For the sake of examples --- the general theory does not rely |
|
15 |
on it! --- a variable of length @{text n} has security level @{text n}: *} |
|
16 |
||
50342 | 17 |
instantiation list :: (type)sec |
18 |
begin |
|
19 |
||
20 |
definition "sec(x :: 'a list) = length x" |
|
21 |
||
22 |
instance .. |
|
23 |
||
24 |
end |
|
25 |
||
26 |
instantiation aexp :: sec |
|
27 |
begin |
|
43158 | 28 |
|
29 |
fun sec_aexp :: "aexp \<Rightarrow> level" where |
|
50342 | 30 |
"sec (N n) = 0" | |
31 |
"sec (V x) = sec x" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50342
diff
changeset
|
32 |
"sec (Plus a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)" |
50342 | 33 |
|
34 |
instance .. |
|
35 |
||
36 |
end |
|
37 |
||
38 |
instantiation bexp :: sec |
|
39 |
begin |
|
43158 | 40 |
|
41 |
fun sec_bexp :: "bexp \<Rightarrow> level" where |
|
50342 | 42 |
"sec (Bc v) = 0" | |
43 |
"sec (Not b) = sec b" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50342
diff
changeset
|
44 |
"sec (And b\<^sub>1 b\<^sub>2) = max (sec b\<^sub>1) (sec b\<^sub>2)" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50342
diff
changeset
|
45 |
"sec (Less a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)" |
50342 | 46 |
|
47 |
instance .. |
|
48 |
||
49 |
end |
|
43158 | 50 |
|
51 |
||
52 |
abbreviation 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 |
||
56 |
abbreviation 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 |
||
60 |
lemma aval_eq_if_eq_le: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50342
diff
changeset
|
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" |
43158 | 62 |
by (induct a) auto |
63 |
||
64 |
lemma bval_eq_if_eq_le: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50342
diff
changeset
|
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" |
43158 | 66 |
by (induct b) (auto simp add: aval_eq_if_eq_le) |
67 |
||
68 |
end |