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