Theory WHATWHERE_Security

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory WHATWHERE_Security
imports Strong_Security.Types
begin

locale WHATWHERE = 
fixes SR :: "('exp, 'id, 'val, 'com) TLSteps"
and E :: "('exp, 'id, 'val) Evalfunction"
and pp :: "'com ⇒ nat"
and DA :: "('id, 'd::order) DomainAssignment"
and lH :: "('d::order, 'exp) lHatches"

begin

― ‹define when two states are indistinguishable for an observer on domain d›
definition d_equal :: "'d::order ⇒ ('id, 'val) State 
  ⇒ ('id, 'val) State ⇒ bool"
where
"d_equal d m m' ≡ ∀x. ((DA x) ≤ d ⟶ (m x) = (m' x))"

abbreviation d_equal' :: "('id, 'val) State 
  ⇒ 'd::order ⇒ ('id, 'val) State ⇒ bool" 
( ‹(_ =⇘_⇙ _)› )
where
"m =⇘d⇙ m' ≡ d_equal d m m'"

― ‹transitivity of d-equality›
lemma d_equal_trans:
"⟦ m =⇘d⇙ m'; m' =⇘d⇙ m'' ⟧ ⟹ m =⇘d⇙ m''"
by (simp add: d_equal_def)


abbreviation SRabbr :: "('exp, 'id, 'val, 'com) TLSteps_curry"
(‹(1⟨_,/_⟩) →⊲_⊳/ (1⟨_,/_⟩)› [0,0,0,0,0] 81)
where
"⟨c,m⟩ →⊲α⊳ ⟨p,m'⟩ ≡ ((c,m),α,(p,m')) ∈ SR"


― ‹function for obtaining the unique memory (state) after one step for a command and a memory (state)›
definition NextMem :: "'com ⇒ ('id, 'val) State ⇒ ('id, 'val) State"
( ‹⟦_⟧'(_')› )
where
"⟦c⟧(m) ≡ (THE m'. (∃p α. ⟨c,m⟩ →⊲α⊳ ⟨p,m'⟩))"

― ‹function getting all escape hatches for some location›
definition htchLoc :: "nat ⇒ ('d, 'exp) Hatches"
where
"htchLoc ι ≡ {(d,e). (d,e,ι) ∈ lH}"

― ‹function for getting all escape hatches for some set of locations›
definition htchLocSet :: "nat set ⇒ ('d, 'exp) Hatches"
where
"htchLocSet PP ≡ ⋃{h. (∃ι ∈ PP. h = htchLoc ι)}"

― ‹predicate for (d,H)-equality›
definition dH_equal :: "'d ⇒ ('d, 'exp) Hatches
  ⇒ ('id, 'val) State ⇒ ('id, 'val) State ⇒ bool"
where
"dH_equal d H m m' ≡ (m =⇘d⇙ m' ∧ 
  (∀(d',e) ∈ H. (d' ≤ d ⟶ (E e m = E e m'))))"

abbreviation dH_equal' :: "('id, 'val) State ⇒ 'd ⇒ ('d, 'exp) Hatches
  ⇒ ('id, 'val) State ⇒ bool"
( ‹(_ ∼⇘_,_⇙ _)› )
where
"m ∼⇘d,H⇙ m' ≡ dH_equal d H m m'"

― ‹predicate indicating that a command is not a d-declassification command›
definition NDC :: "'d ⇒ 'com ⇒ bool"
where
"NDC d c ≡ (∀m m'. m =⇘d⇙ m' ⟶ ⟦c⟧(m) =⇘d⇙ ⟦c⟧(m'))"

― ‹predicate indicating an 'immediate d-declassification command' for a set of escape hatches›
definition IDC :: "'d ⇒ 'com ⇒ ('d, 'exp) Hatches ⇒ bool"
where
"IDC d c H ≡ (∃m m'. m =⇘d⇙ m' ∧ 
  (¬ ⟦c⟧(m) =⇘d⇙ ⟦c⟧(m')))
  ∧ (∀m m'. m ∼⇘d,H⇙ m' ⟶ ⟦c⟧(m) =⇘d⇙ ⟦c⟧(m') )"

definition stepResultsinR :: "'com ProgramState ⇒ 'com ProgramState 
  ⇒ 'com Bisimulation_type ⇒ bool"
where
"stepResultsinR p p' R ≡ (p = None ∧ p' = None) ∨ 
  (∃c c'. (p = Some c ∧ p' = Some c' ∧ ([c],[c']) ∈ R))"


definition dhequality_alternative ::  "'d ⇒ nat set ⇒ nat 
  ⇒ ('id, 'val) State ⇒ ('id, 'val) State ⇒ bool"
where
"dhequality_alternative d PP ι m m' ≡ m ∼⇘d,(htchLocSet PP)⇙ m' ∨
            (¬ (htchLoc ι) ⊆ (htchLocSet PP))"

definition Strong_dlHPP_Bisimulation :: "'d ⇒ nat set 
  ⇒ 'com Bisimulation_type ⇒ bool"
where
"Strong_dlHPP_Bisimulation d PP R ≡ 
  (sym R) ∧ (trans R) ∧
  (∀(V,V') ∈ R. length V = length V') ∧
  (∀(V,V') ∈ R. ∀i < length V. 
    ((NDC d (V!i)) ∨ 
     (IDC d (V!i) (htchLoc (pp (V!i)))))) ∧
  (∀(V,V') ∈ R. ∀i < length V. ∀m1 m1' m2 α p.
    ( ⟨V!i,m1⟩ →⊲α⊳ ⟨p,m2⟩ ∧ m1 ∼⇘d,(htchLocSet PP)⇙ m1')
    ⟶ (∃p' α' m2'. ( ⟨V'!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩ ∧
        (stepResultsinR p p' R) ∧ (α,α') ∈ R ∧ 
        (dhequality_alternative d PP (pp (V!i)) m2 m2'))))"


― ‹predicate to define when a program is strongly secure›
definition WHATWHERE_Secure :: "'com list ⇒ bool"
where
"WHATWHERE_Secure V ≡ (∀d PP. 
  (∃R. Strong_dlHPP_Bisimulation d PP R ∧ (V,V) ∈ R))"


― ‹auxiliary lemma to obtain central strong (d,lH,PP)-Bisimulation property as Lemma
 in meta logic (allows instantiating all the variables manually if necessary)›
lemma strongdlHPPB_aux: 
 "⋀V V' m1 m1' m2 p i α. ⟦ Strong_dlHPP_Bisimulation d PP R;
  i < length V; (V,V') ∈ R; 
  ⟨V!i,m1⟩ →⊲α⊳ ⟨p,m2⟩; m1 ∼⇘d,(htchLocSet PP)⇙ m1' ⟧
 ⟹ (∃p' α' m2'. ⟨V'!i,m1'⟩ →⊲α'⊳ ⟨p',m2'⟩
  ∧ stepResultsinR p p' R ∧ (α,α') ∈ R ∧ 
  (dhequality_alternative d PP (pp (V!i)) m2 m2'))"
  by (simp add: Strong_dlHPP_Bisimulation_def, fastforce)

― ‹auxiliary lemma to obtain 'NDC or IDC' from strong (d,lH,PP)-Bisimulation as lemma
  in meta logic allowing instantiation of the variables›
lemma strongdlHPPB_NDCIDCaux:
"⋀V V' i. ⟦Strong_dlHPP_Bisimulation d PP R;
  (V,V') ∈ R; i < length V ⟧
        ⟹ (NDC d (V!i) ∨ IDC d (V!i) (htchLoc (pp (V!i))))"
  by (simp add: Strong_dlHPP_Bisimulation_def, auto)

lemma WHATWHERE_empty:
"WHATWHERE_Secure []"
  by (simp add: WHATWHERE_Secure_def, auto,
  rule_tac x="{([],[])}" in exI,
  simp add: Strong_dlHPP_Bisimulation_def sym_def trans_def)


end

end