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