Theory WHATWHERE_Secure_Skip_Assign

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory WHATWHERE_Secure_Skip_Assign
imports Parallel_Composition
begin

context WHATWHERE_Secure_Programs
begin

abbreviation NextMem' 
(‹⟦_⟧'(_')›)
where
"⟦c⟧(m) ≡ NextMem c m"

― ‹define when two expressions are indistinguishable with respect to a domain d›
definition d_indistinguishable :: "'d::order ⇒ 'exp ⇒ 'exp ⇒ bool"
where
"d_indistinguishable d e1 e2 ≡ ∀m m'. ((m =⇘d⇙ m') 
  ⟶ ((E e1 m) = (E e2 m')))"

abbreviation d_indistinguishable' :: "'exp ⇒ 'd::order ⇒ 'exp ⇒ bool" 
( ‹(_ ≡⇘_⇙ _)› )
where
"e1 ≡⇘d⇙ e2 ≡ d_indistinguishable d e1 e2"

― ‹symmetry of d-indistinguishable›
lemma d_indistinguishable_sym:
"e ≡⇘d⇙ e' ⟹ e' ≡⇘d⇙ e"
by (simp add: d_indistinguishable_def d_equal_def, metis)

― ‹transitivity of d-indistinguishable›
lemma d_indistinguishable_trans:
"⟦ e ≡⇘d⇙ e'; e' ≡⇘d⇙ e'' ⟧ ⟹ e ≡⇘d⇙ e''"
by (simp add: d_indistinguishable_def d_equal_def, metis)


― ‹predicate for dH-indistinguishable›
definition dH_indistinguishable :: "'d ⇒ ('d, 'exp) Hatches 
  ⇒ 'exp ⇒ 'exp ⇒ bool"
where
"dH_indistinguishable d H e1 e2 ≡ (∀m m'. m ∼⇘d,H⇙ m' 
  ⟶ (E e1 m = E e2 m'))"

abbreviation dH_indistinguishable' :: "'exp ⇒ 'd 
  ⇒ ('d, 'exp) Hatches ⇒ 'exp ⇒ bool" 
( ‹(_ ≡⇘_,_⇙ _)› )
where
"e1 ≡⇘d,H⇙ e2 ≡ dH_indistinguishable d H e1 e2"

lemma empH_implies_dHindistinguishable_eq_dindistinguishable:
"(e ≡⇘d,{}⇙ e') = (e ≡⇘d⇙ e')"
by (simp add: d_indistinguishable_def dH_indistinguishable_def 
  dH_equal_def d_equal_def)


theorem WHATWHERE_Secure_Skip:
"WHATWHERE_Secure [skip⇘ι⇙]"
proof (simp add: WHATWHERE_Secure_def, auto)
  fix d PP
  define R where "R = {(V::('exp,'id) MWLsCom list,V'::('exp,'id) MWLsCom list). 
    V = V' ∧ (V = [] ∨ V = [skip⇘ι⇙])}"
  
  have inR: "([skip⇘ι⇙],[skip⇘ι⇙]) ∈ R"
    by (simp add: R_def)
  
  have "SdlHPPB d PP R"
    proof (simp add: Strong_dlHPP_Bisimulation_def R_def sym_def trans_def
      NDC_def NextMem_def, auto)
      fix m1 m1'
      assume dequal: "m1 =⇘d⇙ m1'"
      have nextm1: "(THE m2. (∃p α. ⟨skip⇘ι⇙,m1⟩ →⊲α⊳ ⟨p,m2⟩)) = m1"
        by (insert MWLsSteps_det.simps[of "skip⇘ι⇙" "m1"], 
          force)
    
      have nextm1': 
        "(THE m2'. (∃p α. ⟨skip⇘ι⇙,m1'⟩ →⊲α⊳ ⟨p,m2'⟩)) = m1'"
        by (insert MWLsSteps_det.simps[of "skip⇘ι⇙" "m1'"], 
          force)
    
      with dequal nextm1 show 
        "THE m2. ∃p α. ⟨skip⇘ι⇙,m1⟩ →⊲α⊳ ⟨p,m2⟩ =⇘d⇙
        THE m2'. ∃p α. ⟨skip⇘ι⇙,m1'⟩ →⊲α⊳ ⟨p,m2'⟩"
        by auto
     next
       fix p m1 m1' m2 α
       assume dequal: "m1 ∼⇘d,(htchLocSet PP)⇙ m1'"
       assume skipstep: "⟨skip⇘ι⇙,m1⟩ →⊲α⊳ ⟨p,m2⟩"
       with  MWLsSteps_det.simps[of "skip⇘ι⇙" "m1" "α" "p" "m2"] 
       have aux: "p = None ∧ m2 = m1 ∧ α = []"
         by auto
       with dequal skipstep MWLsSteps_det.skip
       show "∃p' m2'.
         ⟨skip⇘ι⇙,m1'⟩ →⊲α⊳ ⟨p',m2'⟩ ∧
         stepResultsinR p p' {(V, V'). V = V' ∧ 
         (V = [] ∨ V = [skip⇘ι⇙])} ∧
         (α = [] ∨ α = [skip⇘ι⇙]) ∧
         dhequality_alternative d PP ι m2 m2'"
         by (simp add: stepResultsinR_def dhequality_alternative_def, 
           fastforce)
     qed

     with inR show "∃R. SdlHPPB d PP R ∧ ([skip⇘ι⇙],[skip⇘ι⇙]) ∈ R"
       by auto
qed
 

― ‹auxiliary lemma for assign side condition (lemma 9 in original paper)›
lemma semAssignSC_aux: 
  assumes dhind: "e ≡⇘DA x,(htchLoc ι)⇙ e"
  shows "NDC d (x :=⇘ι⇙ e) ∨ IDC d (x :=⇘ι⇙ e) (htchLoc (pp (x:=⇘ι⇙ e)))"
proof (simp add: IDC_def, auto, simp add: NDC_def)
  fix m1 m1'
  assume dhequal: "m1 ∼⇘d,htchLoc ι⇙ m1'"
  hence dequal: "m1 =⇘d⇙ m1'"
    by (simp add: dH_equal_def)

  obtain v where veq: "E e m1 = v" by auto
  hence m2eq: "⟦x :=⇘ι⇙ e⟧(m1) = m1(x := v)"
    by (simp add: NextMem_def,
      insert MWLsSteps_det.simps[of "x :=⇘ι⇙ e" "m1"],
      force)

  obtain v' where v'eq: "E e m1' = v'" by auto
  hence m2'eq: "⟦x :=⇘ι⇙ e⟧(m1') = m1'(x := v')" 
    by (simp add: NextMem_def,
      insert MWLsSteps_det.simps[of "x :=⇘ι⇙ e" "m1'"],
      force)

  from dhequal have shiftdomain: 
    "DA x ≤ d ⟹ m1 ∼⇘DA x,(htchLoc ι)⇙ m1'"
    by (simp add: dH_equal_def d_equal_def htchLoc_def)

  with veq v'eq dhind
  have "(DA x) ≤ d ⟹ v = v'"
    by (simp add: dH_indistinguishable_def) 

  with dequal m2eq m2'eq
  show "⟦x :=⇘ι⇙ e⟧(m1) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m1')"
    by (simp add: d_equal_def)
qed


theorem WHATWHERE_Secure_Assign:
  assumes dhind: "e ≡⇘DA x,(htchLoc ι)⇙ e"
  assumes dheq_imp: "∀m m' d ι'. (m ∼⇘d,(htchLoc ι')⇙ m' ∧ 
  ⟦x :=⇘ι⇙ e⟧(m) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m'))
  ⟶ ⟦x :=⇘ι⇙ e⟧(m) ∼⇘d,(htchLoc ι')⇙ ⟦x :=⇘ι⇙ e⟧(m')" 
  shows "WHATWHERE_Secure [x :=⇘ι⇙ e]"
proof (simp add: WHATWHERE_Secure_def, auto)
  fix d PP 
  define R where "R = {(V::('exp,'id) MWLsCom list,V'::('exp,'id) MWLsCom list). 
    V = V' ∧ (V = [] ∨ V = [x :=⇘ι⇙ e])}"
  
  have inR: "([x :=⇘ι⇙ e],[x :=⇘ι⇙ e]) ∈ R"
    by (simp add: R_def)
  
  have "SdlHPPB d PP R"
    proof (simp add: Strong_dlHPP_Bisimulation_def R_def 
        sym_def trans_def, auto)
      assume notIDC: "¬ IDC d (x :=⇘ι⇙ e) (htchLoc ι)"
      with dhind semAssignSC_aux
      show "NDC d (x :=⇘ι⇙ e)"
        by force
    next
      fix m1 m1' m2 p α
      assume assignstep: "⟨x :=⇘ι⇙ e,m1⟩ →⊲α⊳ ⟨p,m2⟩"
      assume dhequal: "m1 ∼⇘d,htchLocSet PP⇙ m1'"
      
      from assignstep have nextm1: 
        "p = None ∧ α = [] ∧ ⟦x :=⇘ι⇙ e⟧(m1) = m2"
        by (simp add: NextMem_def, 
          insert MWLsSteps_det.simps[of "x :=⇘ι⇙ e" "m1"], force)
      
      obtain m2' where nextm1': 
        "⟨x :=⇘ι⇙ e,m1'⟩ →⊲[]⊳ ⟨None,m2'⟩ ∧ ⟦x :=⇘ι⇙ e⟧(m1') = m2'"
        by (simp add: NextMem_def, 
          insert MWLsSteps_det.simps[of "x :=⇘ι⇙ e" "m1'"], force)
      
      from dhequal have dhequal_ι: "⋀ι. htchLoc ι ⊆ htchLocSet PP 
        ⟹ m1 ∼⇘d,(htchLoc ι)⇙ m1'"
        by (simp add: dH_equal_def, auto)
      
      with dhind semAssignSC_aux 
      have "htchLoc ι ⊆ htchLocSet PP ⟹ 
        ⟦x :=⇘ι⇙ e⟧(m1) =⇘d⇙ ⟦x :=⇘ι⇙ e⟧(m1')"
        by (simp add: NDC_def IDC_def dH_equal_def, fastforce)
      
      with dhind dheq_imp dhequal_ι 
      have "htchLoc ι ⊆ htchLocSet PP ⟹ 
        ⟦x :=⇘ι⇙ e⟧(m1) ∼⇘d,(htchLocSet PP)⇙ ⟦x :=⇘ι⇙ e⟧(m1')"
        by (simp add: htchLocSet_def dH_equal_def, blast)
      
      with nextm1 nextm1' assignstep dhequal
      show "∃p' m2'.
        ⟨x :=⇘ι⇙ e,m1'⟩ →⊲α⊳ ⟨p',m2'⟩ ∧
        stepResultsinR p p' {(V, V'). V = V' ∧ (V = [] ∨ V = [x:=⇘ι⇙ e])} ∧
        (α = [] ∨ α = [x:=⇘ι⇙ e]) ∧ dhequality_alternative d PP ι m2 m2'"
        by (auto simp add: stepResultsinR_def dhequality_alternative_def)
    qed
  
  with inR show "∃R. SdlHPPB d PP R ∧ ([x:=⇘ι⇙ e],[x:=⇘ι⇙ e]) ∈ R"
    by auto
qed

end

end