Theory Strongly_Secure_Skip_Assign

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

locale Strongly_Secure_Programs =
L? : MWLf_semantics "E" "BMap" 
+ SS?: Strong_Security "MWLfSteps_det" "DA"
for E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val ⇒ bool"
and DA :: "('id, 'd::order) DomainAssignment"
begin 

abbreviation USdBname ::"'d ⇒ ('exp, 'id) MWLfCom Bisimulation_type"
(‹≈⇘_⇙›)
where "≈⇘d⇙ ≡ USdB d" 

abbreviation relatedbyUSdB :: "('exp,'id) MWLfCom list ⇒ 'd
  ⇒ ('exp,'id) MWLfCom list ⇒ bool" (infixr ‹≈⇘_⇙› 65)
where "V ≈⇘d⇙ V' ≡ (V,V') ∈ USdB d"

― ‹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)

theorem Strongly_Secure_Skip:
"[skip] ≈⇘d⇙ [skip]"
proof -
  define R0 where "R0 = {(V::('exp,'id) MWLfCom list,V'::('exp,'id) MWLfCom list). 
    V = [skip] ∧ V' = [skip]}"

  have uptoR0: "d_Bisimulation_Up_To_USdB d R0"
    proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
      show "sym R0" by (simp add: R0_def sym_def)
    next
      fix V V'
      assume "(V,V') ∈ R0"
      thus "length V = length V'"
        by (simp add: R0_def)
    next
      fix V V' i m1 m1' W m2
      assume inR0: "(V,V') ∈ R0"
      assume irange: "i < length V"
      assume step: "⟨V!i,m1⟩ → ⟨W,m2⟩"
      assume dequal: "m1 =⇘d⇙ m1'"
      
      from inR0 have Vassump:
        "V = [skip] ∧ V' = [skip]"
        by (simp add: R0_def)
      
      with step irange have step1:
        "W = [] ∧ m2 = m1"
        by (simp, metis MWLf_semantics.MWLfSteps_det_cases(1))
        
      from Vassump irange obtain m2' where step2:
        "⟨V'!i,m1'⟩ → ⟨[],m2'⟩ ∧ m2' = m1'"
         by (simp, metis MWLfSteps_det.skip)

      with step1 dequal trivialpair_in_USdB show "∃W' m2'.
        ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ 
        ((W,W') ∈ R0 ∨ W ≈⇘d⇙ W') ∧ m2 =⇘d⇙ m2'"
        by auto
   qed
   
   hence "R0 ⊆ ≈⇘d⇙"
     by (rule Up_To_Technique)

   thus ?thesis
     by (simp add: R0_def)

qed

theorem Strongly_Secure_Assign:
  assumes d_indistinguishable_exp: "e ≡⇘DA x⇙ e'"
  shows "[x := e] ≈⇘d⇙ [x := e']"
proof -
  define R0 where "R0 = {(V,V'). ∃x e e'. V = [x := e] ∧ V' = [x := e'] ∧
    e ≡⇘DA x⇙ e'}"

  from d_indistinguishable_exp have inR0: "([x:=e],[x:=e']) ∈ R0"
    by (simp add: R0_def)

  have "d_Bisimulation_Up_To_USdB d R0"
    proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
      from d_indistinguishable_sym show "sym R0"
        by (simp add: R0_def sym_def, fastforce)
    next
      fix V V'
      assume "(V,V') ∈ R0"
      thus "length V = length V'" 
        by (simp add: R0_def, auto)
    next
      fix V V' i m1 m1' W m2
      assume inR0: "(V,V') ∈ R0"
      assume irange: "i < length V"
      assume step: "⟨V!i,m1⟩ → ⟨W,m2⟩"
      assume dequal: "m1 =⇘d⇙ m1'"
      
      from inR0 obtain x e e' where Vassump:
        "V = [x := e] ∧ V' = [x := e'] ∧
        e ≡⇘DA x⇙ e'"
        by (simp add: R0_def, auto)
      
      with step irange obtain v where step1:
        "E e m1 = v ∧ W = [] ∧ m2 = m1(x := v)"
        by (auto, metis MWLf_semantics.MWLfSteps_det_cases(2))
        
      from Vassump irange obtain m2' v' where step2:
        "E e' m1' = v' ∧ ⟨V'!i,m1'⟩ → ⟨[],m2'⟩ ∧ m2' = m1'(x := v')"
        by (auto, metis MWLfSteps_det.assign)

      with Vassump dequal step step1
      have dequalnext: "m1(x := v) =⇘d⇙ m1'(x := v')"      
        by (simp add: d_equal_def d_indistinguishable_def, auto)

      with step1 step2 trivialpair_in_USdB show "∃W' m2'.
        ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ ((W,W') ∈ R0 ∨ W ≈⇘d⇙ W') 
        ∧ m2 =⇘d⇙ m2'"
        by auto
   qed
   
   hence "R0 ⊆ ≈⇘d⇙"
     by (rule Up_To_Technique)

   with inR0 show ?thesis
     by auto

qed

end

end