src/HOL/IMP/Sec_Type_Expr.thy
author kleing
Mon Jun 06 16:29:38 2011 +0200 (2011-06-06)
changeset 43158 686fa0a0696e
child 45200 1f1897ac7877
permissions -rw-r--r--
imported rest of new IMP
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
kleing@43158
    10
text{* The security/confidentiality level of each variable is globally fixed
kleing@43158
    11
for simplicity. For the sake of examples --- the general theory does not rely
kleing@43158
    12
on it! --- a variable of length @{text n} has security level @{text n}: *}
kleing@43158
    13
kleing@43158
    14
definition sec :: "name \<Rightarrow> level" where 
kleing@43158
    15
  "sec n = size n"
kleing@43158
    16
kleing@43158
    17
fun sec_aexp :: "aexp \<Rightarrow> level" where
kleing@43158
    18
"sec_aexp (N n) = 0" |
kleing@43158
    19
"sec_aexp (V x) = sec x" |
kleing@43158
    20
"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
kleing@43158
    21
kleing@43158
    22
fun sec_bexp :: "bexp \<Rightarrow> level" where
kleing@43158
    23
"sec_bexp (B bv) = 0" |
kleing@43158
    24
"sec_bexp (Not b) = sec_bexp b" |
kleing@43158
    25
"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
kleing@43158
    26
"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
kleing@43158
    27
kleing@43158
    28
kleing@43158
    29
abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
kleing@43158
    30
  ("(_ = _ '(\<le> _'))" [51,51,0] 50) where
kleing@43158
    31
"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)"
kleing@43158
    32
kleing@43158
    33
abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
kleing@43158
    34
  ("(_ = _ '(< _'))" [51,51,0] 50) where
kleing@43158
    35
"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
kleing@43158
    36
kleing@43158
    37
lemma aval_eq_if_eq_le:
kleing@43158
    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"
kleing@43158
    39
by (induct a) auto
kleing@43158
    40
kleing@43158
    41
lemma bval_eq_if_eq_le:
kleing@43158
    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"
kleing@43158
    43
by (induct b) (auto simp add: aval_eq_if_eq_le)
kleing@43158
    44
kleing@43158
    45
end