Theory Sec_Type_Expr

section "Security Type Systems"

theory Sec_Type_Expr imports Big_Step
begin

subsection "Security Levels and Expressions"

type_synonym level = nat

class sec =
fixes sec :: "'a ⇒ nat"

text{* The security/confidentiality level of each variable is globally fixed
for simplicity. For the sake of examples --- the general theory does not rely
on it! --- a variable of length @{text n} has security level @{text n}: *}

instantiation list :: (type)sec
begin

definition "sec(x :: 'a list) = length x"

instance ..

end

instantiation aexp :: sec
begin

fun sec_aexp :: "aexp ⇒ level" where
"sec (N n) = 0" |
"sec (V x) = sec x" |
"sec (Plus a⇩1 a⇩2) = max (sec a⇩1) (sec a⇩2)"

instance ..

end

instantiation bexp :: sec
begin

fun sec_bexp :: "bexp ⇒ level" where
"sec (Bc v) = 0" |
"sec (Not b) = sec b" |
"sec (And b⇩1 b⇩2) = max (sec b⇩1) (sec b⇩2)" |
"sec (Less a⇩1 a⇩2) = max (sec a⇩1) (sec a⇩2)"

instance ..

end


abbreviation eq_le :: "state ⇒ state ⇒ level ⇒ bool"
  ("(_ = _ '(≤ _'))" [51,51,0] 50) where
"s = s' (≤ l) == (∀ x. sec x ≤ l ⟶ s x = s' x)"

abbreviation eq_less :: "state ⇒ state ⇒ level ⇒ bool"
  ("(_ = _ '(< _'))" [51,51,0] 50) where
"s = s' (< l) == (∀ x. sec x < l ⟶ s x = s' x)"

lemma aval_eq_if_eq_le:
  "⟦ s⇩1 = s⇩2 (≤ l);  sec a ≤ l ⟧ ⟹ aval a s⇩1 = aval a s⇩2"
by (induct a) auto

lemma bval_eq_if_eq_le:
  "⟦ s⇩1 = s⇩2 (≤ l);  sec b ≤ l ⟧ ⟹ bval b s⇩1 = bval b s⇩2"
by (induct b) (auto simp add: aval_eq_if_eq_le)

end