Theory Asymptotic_Security

theory Asymptotic_Security imports Concrete_Security begin

section ‹Asymptotic security definition›

locale constructive_security_obsf' =
  fixes real_resource :: "security ⇒ ('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "security ⇒ ('c + 'e, 'd + 'f) resource"
    and sim :: "security ⇒ ('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "security ⇒ ('a, 'b) ℐ"
    and ℐ_ideal :: "security ⇒ ('c, 'd) ℐ"
    and ℐ_common :: "security ⇒ ('e, 'f) ℐ"
    and 𝒜 :: "security ⇒ ('a + 'e, 'b + 'f) distinguisher_obsf"
  assumes constructive_security_aux_obsf: "⋀η.
    constructive_security_aux_obsf (real_resource η) (ideal_resource η) (sim η) (ℐ_real η) (ℐ_ideal η) (ℐ_common η) 0"
    and adv: "⟦ ⋀η. exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η) ⊢g 𝒜 η √ ⟧
      ⟹ negligible (λη. advantage (𝒜 η) (obsf_resource (sim η |= 1C ⊳ ideal_resource η)) (obsf_resource (real_resource η)))"
begin

sublocale constructive_security_aux_obsf 
  "real_resource η"
  "ideal_resource η"
  "sim η" 
  "ℐ_real η"
  "ℐ_ideal η"
  "ℐ_common η"
  "0"
  for η by(rule constructive_security_aux_obsf)

lemma constructive_security_obsf'D:
  "constructive_security_obsf (real_resource η) (ideal_resource η) (sim η) (ℐ_real η) (ℐ_ideal η) (ℐ_common η) (𝒜 η)
    (advantage (𝒜 η) (obsf_resource (sim η |= 1C ⊳ ideal_resource η)) (obsf_resource (real_resource η)))"
  by(rule constructive_security_obsf_refl)

end

lemma constructive_security_obsf'I:
  assumes "⋀η. constructive_security_obsf (real_resource η) (ideal_resource η) (sim η) (ℐ_real η) (ℐ_ideal η) (ℐ_common η) (𝒜 η) (adv η)"
    and "(⋀η. exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η) ⊢g 𝒜 η √) ⟹ negligible adv"
  shows "constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common 𝒜"
proof -
  interpret constructive_security_obsf 
    "real_resource η"
    "ideal_resource η"
    "sim η" 
    "ℐ_real η"
    "ℐ_ideal η"
    "ℐ_common η"
    "𝒜 η"
    "adv η"
    for η by fact
  show ?thesis 
  proof
    show "negligible (λη. advantage (𝒜 η) (obsf_resource (sim η |= 1C ⊳ ideal_resource η)) (obsf_resource (real_resource η)))"
      if "⋀η. exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η) ⊢g 𝒜 η √" using assms(2)[OF that]
      by(rule negligible_mono)(auto intro!: eventuallyI landau_o.big_mono simp add: advantage_nonneg adv_nonneg adv[OF that])
  qed(rule WT_intro pfinite_intro order_refl)+
qed

lemma constructive_security_obsf'_into_constructive_security:
  assumes "⋀𝒜 :: security ⇒ ('a + 'b, 'c + 'd) distinguisher_obsf. 
   ⟦  ⋀η. interaction_bounded_by (λ_. True) (𝒜 η) (bound η);
      ⋀η. lossless ⟹ plossless_gpv (exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η)) (𝒜 η) ⟧
   ⟹ constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common 𝒜"
    and correct: "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕ℐ ℐ_common η ⊢g 𝒟 η √) ⟶
               (∀η. interaction_any_bounded_by (𝒟 η) (bound η)) ⟶
               (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕ℐ ℐ_common η) (𝒟 η)) ⟶
               (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
               Negligible.negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |= 1C ⊳ real_resource η))"
  shows "constructive_security real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common bound lossless w"
proof
  interpret constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common ‹λ_. Done undefined›
    by(rule assms) simp_all 
  show "ℐ_real η ⊕ℐ ℐ_common η ⊢res real_resource η √" 
    and "ℐ_ideal η ⊕ℐ ℐ_common η ⊢res ideal_resource η √"
    and "ℐ_real η, ℐ_ideal η ⊢C sim η √" for η by(rule WT_intro)+ 

  show "∃cnv. ∀𝒟. (∀η. ℐ_ideal η ⊕ℐ ℐ_common η ⊢g 𝒟 η √) ⟶
               (∀η. interaction_any_bounded_by (𝒟 η) (bound η)) ⟶
               (∀η. lossless ⟶ plossless_gpv (ℐ_ideal η ⊕ℐ ℐ_common η) (𝒟 η)) ⟶
               (∀η. wiring (ℐ_ideal η) (ℐ_real η) (cnv η) (w η)) ∧
               Negligible.negligible (λη. advantage (𝒟 η) (ideal_resource η) (cnv η |= 1C ⊳ real_resource η))"
    by fact
next
  fix 𝒜 :: "security ⇒ ('a + 'b, 'c + 'd) distinguisher"
  assume WT_adv [WT_intro]: "⋀η. ℐ_real η ⊕ℐ ℐ_common η ⊢g 𝒜 η √"
    and bound [interaction_bound]: "⋀η. interaction_any_bounded_by (𝒜 η) (bound η)"
    and lossless: "⋀η. lossless ⟹ plossless_gpv (ℐ_real η ⊕ℐ ℐ_common η) (𝒜 η)"
  let ?𝒜 = "λη. obsf_distinguisher (𝒜 η)"
  interpret constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common ?𝒜
  proof(rule assms)
    show "interaction_any_bounded_by (?𝒜 η) (bound η)" for η by(rule interaction_bound)+
    show "plossless_gpv (exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η)) (?𝒜 η)" if lossless for η
      using WT_adv[of η] lossless that by(simp)
  qed
  have "negligible (λη. advantage (?𝒜 η) (obsf_resource (sim η |= 1C ⊳ ideal_resource η)) (obsf_resource (real_resource η)))"
    by(rule adv)(rule WT_intro)+
  then show "negligible (λη. advantage (𝒜 η) (sim η |= 1C ⊳ ideal_resource η) (real_resource η))"
    unfolding advantage_obsf_distinguisher .
qed

subsection ‹Composition theorems›

theorem constructive_security_obsf'_composability:
  fixes real
  assumes "constructive_security_obsf' middle ideal sim_inner ℐ_middle ℐ_inner ℐ_common (λη. absorb (𝒜 η) (obsf_converter (sim_outer η |= 1C)))"
  assumes "constructive_security_obsf' real middle sim_outer ℐ_real ℐ_middle ℐ_common 𝒜"
  shows "constructive_security_obsf' real ideal (λη. sim_outer η ⊙ sim_inner η) ℐ_real ℐ_inner ℐ_common 𝒜"
proof(rule constructive_security_obsf'I)
  let ?𝒜 = "λη. absorb (𝒜 η) (obsf_converter (sim_outer η |= 1C))"
  interpret inner: constructive_security_obsf' middle ideal sim_inner ℐ_middle ℐ_inner ℐ_common ?𝒜 by fact
  interpret outer: constructive_security_obsf' real middle sim_outer ℐ_real ℐ_middle ℐ_common 𝒜 by fact

  let ?adv1 = "λη. advantage (?𝒜 η) (obsf_resource (sim_inner η |= 1C ⊳ ideal η)) (obsf_resource (middle η))"
  let ?adv2 = "λη. advantage (𝒜 η) (obsf_resource (sim_outer η |= 1C ⊳ middle η)) (obsf_resource (real η))"
  let ?adv = "λη. ?adv1 η + ?adv2 η"    
  show "constructive_security_obsf (real η) (ideal η) (sim_outer η ⊙ sim_inner η) (ℐ_real η) (ℐ_inner η) (ℐ_common η) (𝒜 η) (?adv η)" for η
    using inner.constructive_security_obsf'D outer.constructive_security_obsf'D
    by(rule constructive_security_obsf_composability)
  assume [WT_intro]: "exception_ℐ (ℐ_real η ⊕ℐ ℐ_common η) ⊢g 𝒜 η √" for η
  have "negligible ?adv1" by(rule inner.adv)(rule WT_intro)+
  also have "negligible ?adv2" by(rule outer.adv)(rule WT_intro)+
  finally (negligible_plus) show "negligible ?adv" .
qed

theorem constructive_security_obsf'_lifting: (* TODO: generalize! *)
  assumes sec: "constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common (λη. absorb (𝒜 η) (obsf_converter (1C |= conv η)))"
  assumes WT_conv [WT_intro]: "⋀η. ℐ_common' η, ℐ_common η ⊢C conv η √"
    and pfinite [pfinite_intro]: "⋀η. pfinite_converter (ℐ_common' η) (ℐ_common η) (conv η)"
  shows "constructive_security_obsf'
     (λη. 1C |= conv η ⊳ real_resource η) (λη. 1C |= conv η ⊳ ideal_resource η) sim
     ℐ_real ℐ_ideal ℐ_common' 𝒜"
proof(rule constructive_security_obsf'I)
  let ?𝒜 = "λη. absorb (𝒜 η) (obsf_converter (1C |= conv η))"
  interpret constructive_security_obsf' real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common ?𝒜 by fact
  let ?adv = "λη. advantage (?𝒜 η) (obsf_resource (sim η |= 1C ⊳ ideal_resource η)) (obsf_resource (real_resource η))" 

  fix η :: security
  show "constructive_security_obsf (1C |= conv η ⊳ real_resource η) (1C |= conv η ⊳ ideal_resource η) (sim η)
     (ℐ_real η) (ℐ_ideal η) (ℐ_common' η) (𝒜 η)
     (?adv η)"
    using constructive_security_obsf.constructive_security_aux_obsf[OF constructive_security_obsf'D]
     constructive_security_obsf.constructive_security_sim_obsf[OF constructive_security_obsf'D]
    by(rule constructive_security_obsf_lifting_usr)(rule WT_intro pfinite_intro)+
  show "negligible ?adv" if [WT_intro]: "⋀η. exception_ℐ (ℐ_real η ⊕ℐ ℐ_common' η) ⊢g 𝒜 η √"
    by(rule adv)(rule WT_intro)+
qed

theorem constructive_security_obsf'_trivial:
  fixes res
  assumes [WT_intro]: "⋀η. ℐ η ⊕ℐ ℐ_common η ⊢res res η √"
  shows "constructive_security_obsf' res res (λ_. 1C) ℐ ℐ ℐ_common 𝒜"
proof(rule constructive_security_obsf'I)
  show "constructive_security_obsf (res η) (res η) 1C (ℐ η) (ℐ η) (ℐ_common η) (𝒜 η) 0" for η
    using assms by(rule constructive_security_obsf_trivial)
qed simp

theorem parallel_constructive_security_obsf':
  assumes "constructive_security_obsf' real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 (λη. absorb (𝒜 η) (obsf_converter (parallel_wiring ⊙ parallel_converter 1C (converter_of_resource (sim2 η |= 1C ⊳ ideal2 η)))))"
    (is "constructive_security_obsf' _ _ _ _ _ _ ?𝒜1")
  assumes "constructive_security_obsf' real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 (λη. absorb (𝒜 η) (obsf_converter (parallel_wiring ⊙ parallel_converter (converter_of_resource (real1 η)) 1C)))"
    (is "constructive_security_obsf' _ _ _ _ _ _ ?𝒜2")
  shows "constructive_security_obsf' (λη. parallel_wiring ⊳ real1 η ∥ real2 η) (λη. parallel_wiring ⊳ ideal1 η ∥ ideal2 η) (λη. sim1 η |= sim2 η) 
    (λη. ℐ_real1 η ⊕ℐ ℐ_real2 η) (λη. ℐ_inner1 η ⊕ℐ ℐ_inner2 η) (λη. ℐ_common1 η ⊕ℐ ℐ_common2 η) 𝒜"
proof(rule constructive_security_obsf'I)
  interpret sec1: constructive_security_obsf' real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 ?𝒜1 by fact
  interpret sec2: constructive_security_obsf' real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 ?𝒜2 by fact
  let ?adv1 = "λη. advantage (?𝒜1 η) (obsf_resource (sim1 η |= 1C ⊳ ideal1 η)) (obsf_resource (real1 η))"
  let ?adv2 = "λη. advantage (?𝒜2 η) (obsf_resource (sim2 η |= 1C ⊳ ideal2 η)) (obsf_resource (real2 η))"
  let ?adv = "λη. ?adv1 η + ?adv2 η"
  show "constructive_security_obsf (parallel_wiring ⊳ real1 η ∥ real2 η) (parallel_wiring ⊳ ideal1 η ∥ ideal2 η)
     (sim1 η |= sim2 η) (ℐ_real1 η ⊕ℐ ℐ_real2 η) (ℐ_inner1 η ⊕ℐ ℐ_inner2 η) (ℐ_common1 η ⊕ℐ ℐ_common2 η) (𝒜 η)
     (?adv η)" for η
    using sec1.constructive_security_obsf'D sec2.constructive_security_obsf'D
    by(rule parallel_constructive_security_obsf)
  assume [WT_intro]: "exception_ℐ ((ℐ_real1 η ⊕ℐ ℐ_real2 η) ⊕ℐ (ℐ_common1 η ⊕ℐ ℐ_common2 η)) ⊢g 𝒜 η √" for η
  have "negligible ?adv1" by(rule sec1.adv)(rule WT_intro)+
  also have "negligible ?adv2" by(rule sec2.adv)(rule WT_intro)+
  finally (negligible_plus) show "negligible ?adv" .
qed

end