header "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