src/HOL/IMP/Sec_Type_Expr.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 50342 e77b0dbcae5b
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     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 :: "vname \<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 (Bc v) = 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