src/HOL/IMP/Sec_Type_Expr.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 section "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 class sec =
    11 fixes sec :: "'a \<Rightarrow> nat"
    12 
    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 
    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
    28 
    29 fun 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 
    34 instance ..
    35 
    36 end
    37 
    38 instantiation bexp :: sec
    39 begin
    40 
    41 fun 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 
    47 instance ..
    48 
    49 end
    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:
    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"
    62 by (induct a) auto
    63 
    64 lemma 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"
    66 by (induct b) (auto simp add: aval_eq_if_eq_le)
    67 
    68 end