Theory Strong_Security

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

locale Strong_Security = 
fixes SR :: "('exp, 'id, 'val, 'com) TSteps"
and DA :: "('id, 'd::order) DomainAssignment"

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) TSteps_curry"
("(1⟨_,/_⟩) →/ (1⟨_,/_⟩)" [0,0,0,0] 81)
where
"⟨c,m⟩ → ⟨c',m'⟩ ≡ ((c,m),(c',m')) ∈ SR"

― ‹predicate for strong d-bisimulation›
definition Strong_d_Bisimulation :: "'d ⇒ 'com Bisimulation_type ⇒ bool"
where
"Strong_d_Bisimulation d R ≡ 
  (sym R) ∧
  (∀(V,V') ∈ R. length V = length V') ∧
  (∀(V,V') ∈ R. ∀i < length V. ∀m1 m1' m2 W.
  ⟨V!i,m1⟩ → ⟨W,m2⟩ ∧ m1 =⇘d⇙ m1'
  ⟶ (∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ (W,W') ∈ R ∧ m2 =⇘d⇙ m2'))"

― ‹union of all strong d-bisimulations›
definition USdB :: "'d ⇒ 'com Bisimulation_type"
("≈⇘_⇙" 65)
where
"≈⇘d⇙ ≡ ⋃{r. (Strong_d_Bisimulation d r)}"

abbreviation relatedbyUSdB :: "'com list ⇒ 'd ⇒ 'com list ⇒ bool" 
("(_ ≈⇘_⇙ _)" [66,66] 65)
where "V ≈⇘d⇙ V' ≡ (V,V') ∈ USdB d"

― ‹predicate to define when a program is strongly secure›
definition Strongly_Secure :: "'com list ⇒ bool"
where
"Strongly_Secure V ≡ (∀d. V ≈⇘d⇙ V)"


― ‹auxiliary lemma to obtain central strong d-Bisimulation property as Lemma
 in meta logic (allows instantiating all the variables manually if necessary)›
lemma strongdB_aux: "⋀V V' m1 m1' m2 W i. ⟦ Strong_d_Bisimulation d R;
 i < length V ; (V,V') ∈ R; ⟨V!i,m1⟩ → ⟨W,m2⟩; m1 =⇘d⇙ m1' ⟧
 ⟹ (∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ (W,W') ∈ R ∧ m2 =⇘d⇙ m2')"
by (simp add: Strong_d_Bisimulation_def, fastforce)

lemma trivialpair_in_USdB:
"[] ≈⇘d⇙ []"
by (simp add: USdB_def Strong_d_Bisimulation_def, 
  rule_tac x="{([],[])}" in exI, simp add: sym_def)

lemma USdBsym: "sym (≈⇘d⇙)"
by (simp add: USdB_def Strong_d_Bisimulation_def sym_def, auto)

lemma USdBeqlen: 
  "V ≈⇘d⇙ V' ⟹ length V = length V'"
by (simp add: USdB_def Strong_d_Bisimulation_def, auto)              

lemma USdB_Strong_d_Bisimulation:
  "Strong_d_Bisimulation d (≈⇘d⇙)"
proof (simp add: Strong_d_Bisimulation_def, auto)
  show "sym (≈⇘d⇙)" by (rule USdBsym)
next
  fix V V'
  show "V ≈⇘d⇙ V' ⟹ length V = length V'" by (rule USdBeqlen, auto)
next
  fix V V' m1 m1' m2 W i
  assume inUSdB: "V ≈⇘d⇙ V'"
  assume stepV: "⟨V!i,m1⟩ → ⟨W,m2⟩"
  assume irange: "i < length V"
  assume dequal: "m1 =⇘d⇙ m1'"
  
  from inUSdB obtain R where someR:
    "Strong_d_Bisimulation d R ∧ (V,V') ∈ R" 
    by (simp add: USdB_def, auto)

  with strongdB_aux stepV irange dequal show 
    "∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ W ≈⇘d⇙ W' ∧ m2 =⇘d⇙ m2'"
    by (simp add: USdB_def, fastforce)
      
qed


lemma USdBtrans: "trans (≈⇘d⇙)"
proof (simp add: trans_def, auto)
  fix V V' V''
  assume p1: "V ≈⇘d⇙ V'"
  assume p2: "V' ≈⇘d⇙ V''"

  let ?R = "{(V,V''). ∃V'. V ≈⇘d⇙ V' ∧ V' ≈⇘d⇙ V''}"

  from p1 p2 have inRest: "(V,V'') ∈ ?R" by auto

  have SdB_rest: "Strong_d_Bisimulation d ?R"
    proof (simp add: Strong_d_Bisimulation_def sym_def, auto)
        fix V V' V''
        assume p1: "V ≈⇘d⇙ V'"
        moreover
        assume p2: "V' ≈⇘d⇙ V''"
        moreover
        from p1 USdBsym have "V' ≈⇘d⇙ V" 
          by (simp add: sym_def)
        moreover
        from p2 USdBsym have "V'' ≈⇘d⇙ V'" 
          by (simp add: sym_def)
        ultimately show  
        "∃V'. V'' ≈⇘d⇙ V' ∧ V' ≈⇘d⇙ V"
          by (rule_tac x="V'" in exI, auto)
      next
        fix V V' V''
        assume p1: "V ≈⇘d⇙ V'"
        moreover
        assume p2: "V' ≈⇘d⇙ V''"
        moreover
        from p1 USdBeqlen[of "V" "V'"] have "length V = length V'"
          by auto
        moreover 
        from p2 USdBeqlen[of "V'" "V''"] have "length V' = length V''"
          by auto
        ultimately show eqlen: "length V = length V''" by auto
      next
        fix V V' V'' i m1 m1' W m2
        assume step: "⟨V!i,m1⟩ → ⟨W,m2⟩"
        assume dequal: "m1 =⇘d⇙ m1'"
        assume p1: "V ≈⇘d⇙ V'"
        assume p2: "V' ≈⇘d⇙ V''"
        assume irange: "i < length V"
        from p1 USdBeqlen[of "V" "V'"] 
        have leq: "length V = length V'"
          by force
          
        have deq_same: "m1' =⇘d⇙ m1'" by (simp add: d_equal_def)

        from irange step dequal p1 USdB_Strong_d_Bisimulation 
          strongdB_aux[of "d" "≈⇘d⇙" "i" "V" "V'" "m1" "W" "m2" "m1'"]
        obtain W' m2' where p1concl: 
          "⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧ W ≈⇘d⇙ W' ∧ m2 =⇘d⇙ m2'"
          by auto
        
        with deq_same leq USdB_Strong_d_Bisimulation
          strongdB_aux[of "d" "≈⇘d⇙" "i" "V'" "V''" "m1'" "W'" "m2'" "m1'"]
          irange p2 dequal obtain W'' m2'' where p2concl:
          "W' ≈⇘d⇙ W'' ∧ ⟨V''!i,m1'⟩ → ⟨W'',m2''⟩ ∧ m2' =⇘d⇙ m2''"
          by auto   

        from p1concl p2concl d_equal_trans have tt'': "m2 =⇘d⇙ m2''"
          by blast

        from p1concl p2concl have "(W,W'') ∈ ?R"
          by auto
        
        with p2concl tt'' show "∃W'' m2''. ⟨V''!i,m1'⟩ → ⟨W'',m2''⟩ ∧ 
          (∃V'. W ≈⇘d⇙ V' ∧ V' ≈⇘d⇙ W'') ∧ m2 =⇘d⇙ m2''"
          by auto
    qed  

  hence liftup: "?R ⊆ (≈⇘d⇙)" 
    by (simp add: USdB_def, auto)

  with inRest show "V ≈⇘d⇙ V''"
    by auto

qed


end

end