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⟨_,/_⟩) ->\<lhd>_\<rhd>/ (1⟨_,/_⟩)" [0,0,0,0,0] 81)
where
"⟨c,m⟩ ->\<lhd>α\<rhd> ⟨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⟩ ->\<lhd>α\<rhd> ⟨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 ≡ \<Union>{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⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩ ∧ m1 ∼⇘d,(htchLocSet PP)⇙ m1')
    --> (∃p' α' m2'. ( ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨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⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩; m1 ∼⇘d,(htchLocSet PP)⇙ m1' |]
 ==> (∃p' α' m2'. ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨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