src/HOL/IMP/Sec_Type_Expr.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45212 e87feee00a4c
child 50342 e77b0dbcae5b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
header "Security Type Systems"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory Sec_Type_Expr imports Big_Step
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
subsection "Security Levels and Expressions"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
type_synonym level = nat
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
text{* The security/confidentiality level of each variable is globally fixed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
for simplicity. For the sake of examples --- the general theory does not rely
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
on it! --- a variable of length @{text n} has security level @{text n}: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45200
diff changeset
    14
definition sec :: "vname \<Rightarrow> level" where 
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
  "sec n = size n"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
fun sec_aexp :: "aexp \<Rightarrow> level" where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
"sec_aexp (N n) = 0" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
"sec_aexp (V x) = sec x" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
fun sec_bexp :: "bexp \<Rightarrow> level" where
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 43158
diff changeset
    23
"sec_bexp (Bc v) = 0" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
"sec_bexp (Not b) = sec_bexp b" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
  ("(_ = _ '(\<le> _'))" [51,51,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
  ("(_ = _ '(< _'))" [51,51,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
lemma aval_eq_if_eq_le:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    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"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
by (induct a) auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
lemma bval_eq_if_eq_le:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    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"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
by (induct b) (auto simp add: aval_eq_if_eq_le)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
end