Theory Concrete_Security

theory Concrete_Security 
imports 
  Observe_Failure
  Construction_Utility
begin

section ‹Concrete security definition›

locale constructive_security_aux_obsf =
  fixes real_resource :: "('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "('c + 'e, 'd + 'f) resource"
    and sim :: "('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "('a, 'b) ℐ"
    and ℐ_ideal :: "('c, 'd) ℐ"
    and ℐ_common :: "('e, 'f) ℐ"
    and adv :: real
  assumes WT_real [WT_intro]: "ℐ_real ⊕⇩ℐ ℐ_common ⊢res real_resource √"
    and WT_ideal [WT_intro]: "ℐ_ideal ⊕⇩ℐ ℐ_common ⊢res ideal_resource √"
    and WT_sim [WT_intro]: "ℐ_real, ℐ_ideal ⊢⇩C sim √"
    and pfinite_sim [pfinite_intro]: "pfinite_converter ℐ_real ℐ_ideal sim"
    and adv_nonneg: "0 ≤ adv"

locale constructive_security_sim_obsf =
  fixes real_resource :: "('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "('c + 'e, 'd + 'f) resource"
    and sim :: "('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "('a, 'b) ℐ"
    and ℐ_common :: "('e, 'f) ℐ"
    and 𝒜 :: "('a + 'e, 'b + 'f) distinguisher_obsf"
    and adv :: real
  assumes adv: "⟦ exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢g 𝒜 √ ⟧
      ⟹ advantage 𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource (real_resource)) ≤ adv"

locale constructive_security_obsf = constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common adv
  + constructive_security_sim_obsf real_resource ideal_resource sim ℐ_real ℐ_common 𝒜 adv
  for real_resource :: "('a + 'e, 'b + 'f) resource"
    and ideal_resource :: "('c + 'e, 'd + 'f) resource"
    and sim :: "('a, 'b, 'c, 'd) converter"
    and ℐ_real :: "('a, 'b) ℐ"
    and ℐ_ideal :: "('c, 'd) ℐ"
    and ℐ_common :: "('e, 'f) ℐ"
    and 𝒜 :: "('a + 'e, 'b + 'f) distinguisher_obsf"
    and adv :: real
begin

lemma constructive_security_aux_obsf: "constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common adv" ..
lemma constructive_security_sim_obsf: "constructive_security_sim_obsf real_resource ideal_resource sim ℐ_real ℐ_common 𝒜 adv" ..

end

context constructive_security_aux_obsf begin

lemma constructive_security_obsf_refl:
  "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common 𝒜
    (advantage 𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource (real_resource)))"
  by unfold_locales(simp_all add: advantage_def WT_intro pfinite_intro)

end

lemma constructive_security_obsf_absorb_cong:
  assumes sec: "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common (absorb 𝒜 cnv) adv"
    and [WT_intro]: "exception_ℐ ℐ, exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢⇩C cnv √" "exception_ℐ ℐ, exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢⇩C cnv' √" "exception_ℐ ℐ ⊢g 𝒜 √"
    and cong: "exception_ℐ ℐ, exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢⇩C cnv ∼ cnv'"
  shows "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common (absorb 𝒜 cnv') adv"
proof -
  interpret constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common "absorb 𝒜 cnv" adv by fact
  show ?thesis
  proof
    have "connect_obsf 𝒜 (cnv' ⊳ obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) = connect_obsf 𝒜 (cnv ⊳ obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource))"
      "connect_obsf 𝒜 (cnv' ⊳ obsf_resource real_resource) = connect_obsf 𝒜 (cnv ⊳ obsf_resource real_resource)"
      by(rule connect_eq_resource_cong eq_ℐ_attach_on' WT_intro cong[symmetric] order_refl)+
    then have "advantage (absorb 𝒜 cnv') (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource) =
          advantage (absorb 𝒜 cnv) (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource)"
      unfolding advantage_def distinguish_attach[symmetric] by simp
    also have "… ≤ adv" by(rule adv)(rule WT_intro)+
    finally show "advantage (absorb 𝒜 cnv') (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource) ≤ adv" .
  qed
qed

lemma constructive_security_obsf_sim_cong:
  assumes sec: "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common 𝒜 adv"
    and cong: "ℐ_real, ℐ_ideal ⊢⇩C sim ∼ sim'"
    and pfinite [pfinite_intro]: "pfinite_converter ℐ_real ℐ_ideal sim'" (* This could probably be derived from cong and sec.pfinite_sim *)
  shows "constructive_security_obsf real_resource ideal_resource sim' ℐ_real ℐ_ideal ℐ_common 𝒜 adv"
proof
  interpret constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common 𝒜 adv by fact
  show "ℐ_real ⊕⇩ℐ ℐ_common ⊢res real_resource √" "ℐ_ideal ⊕⇩ℐ ℐ_common ⊢res ideal_resource √" by(rule WT_intro)+
  from cong show [WT_intro]: "ℐ_real, ℐ_ideal ⊢⇩C sim' √" by(rule eq_ℐ_converterD_WT1)(rule WT_intro)
  show "pfinite_converter ℐ_real ℐ_ideal sim'" by fact
  show "0 ≤ adv" by(rule adv_nonneg)

  assume WT [WT_intro]: "exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢g 𝒜 √"
  have "connect_obsf 𝒜 (obsf_resource (sim' |⇩= 1⇩C ⊳ ideal_resource)) = connect_obsf 𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource))"
    by(rule connect_eq_resource_cong WT_intro obsf_resource_eq_ℐ_cong eq_ℐ_attach_on' parallel_converter2_eq_ℐ_cong cong[symmetric] eq_ℐ_converter_reflI | simp)+
  with adv[OF WT]
  show "advantage 𝒜 (obsf_resource (sim' |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource) ≤ adv"
    unfolding advantage_def by simp
qed

lemma constructive_security_obsfI_core_rest [locale_witness]:
  assumes "constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal (ℐ_common_core ⊕⇩ℐ ℐ_common_rest) adv"
    and adv: "⟦ exception_ℐ (ℐ_real ⊕⇩ℐ (ℐ_common_core ⊕⇩ℐ ℐ_common_rest)) ⊢g 𝒜 √ ⟧
      ⟹ advantage 𝒜 (obsf_resource (sim |⇩= (1⇩C |⇩= 1⇩C) ⊳ ideal_resource)) (obsf_resource (real_resource)) ≤ adv"
  shows "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal (ℐ_common_core ⊕⇩ℐ ℐ_common_rest) 𝒜 adv"
proof -
  interpret constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal "ℐ_common_core ⊕⇩ℐ ℐ_common_rest" by fact
  show ?thesis
  proof
    assume A [WT_intro]: "exception_ℐ (ℐ_real ⊕⇩ℐ (ℐ_common_core ⊕⇩ℐ ℐ_common_rest)) ⊢g 𝒜 √"
    hence outs: "outs_gpv (exception_ℐ (ℐ_real ⊕⇩ℐ (ℐ_common_core ⊕⇩ℐ ℐ_common_rest))) 𝒜 ⊆ outs_ℐ (ℐ_real ⊕⇩ℐ (ℐ_common_core ⊕⇩ℐ ℐ_common_rest))"
      unfolding WT_gpv_iff_outs_gpv by simp
    have "connect_obsf 𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) = connect_obsf 𝒜 (obsf_resource (sim |⇩= 1⇩C |⇩= 1⇩C ⊳ ideal_resource))"
      by(rule connect_cong_trace trace_eq_obsf_resourceI eq_resource_on_imp_trace_eq eq_ℐ_attach_on')+
        (rule WT_intro parallel_converter2_eq_ℐ_cong eq_ℐ_converter_reflI parallel_converter2_id_id[symmetric] order_refl outs)+
    then show "advantage 𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource) ≤ adv" 
      using adv[OF A] by(simp add: advantage_def)
  qed
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 |⇩= 1⇩C))) adv1"
  assumes "constructive_security_obsf real middle sim_outer ℐ_real ℐ_middle ℐ_common 𝒜 adv2"
  shows "constructive_security_obsf real ideal (sim_outer ⊙ sim_inner) ℐ_real ℐ_inner ℐ_common 𝒜 (adv1 + adv2)"
proof
  let ?𝒜 = "absorb 𝒜 (obsf_converter (sim_outer |⇩= 1⇩C))"
  interpret inner: constructive_security_obsf middle ideal sim_inner ℐ_middle ℐ_inner ℐ_common ?𝒜 adv1 by fact
  interpret outer: constructive_security_obsf real middle sim_outer ℐ_real ℐ_middle ℐ_common 𝒜 adv2 by fact

  show "ℐ_real ⊕⇩ℐ ℐ_common ⊢res real √"
    and "ℐ_inner ⊕⇩ℐ ℐ_common ⊢res ideal √"
    and "ℐ_real, ℐ_inner ⊢⇩C sim_outer ⊙ sim_inner √"  by(rule WT_intro)+
  show "pfinite_converter ℐ_real ℐ_inner (sim_outer ⊙ sim_inner)" by(rule pfinite_intro WT_intro)+
  show "0 ≤ adv1 + adv2" using inner.adv_nonneg outer.adv_nonneg by simp

  assume WT_adv[WT_intro]: "exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common) ⊢g 𝒜 √"
  have eq1: "connect_obsf (absorb 𝒜 (obsf_converter (sim_outer |⇩= 1⇩C))) (obsf_resource (sim_inner |⇩= 1⇩C ⊳ ideal)) = 
      connect_obsf 𝒜 (obsf_resource (sim_outer ⊙ sim_inner |⇩= 1⇩C ⊳ ideal))"
    unfolding distinguish_attach[symmetric]
    apply(rule connect_eq_resource_cong)
      apply(rule WT_intro)
     apply(simp del: outs_plus_ℐ add: parallel_converter2_comp1_out attach_compose)
     apply(rule obsf_attach)
       apply(rule pfinite_intro WT_intro)+
    done
  have eq2: "connect_obsf (absorb 𝒜 (obsf_converter (sim_outer |⇩= 1⇩C))) (obsf_resource middle) =
      connect_obsf 𝒜 (obsf_resource (sim_outer |⇩= 1⇩C ⊳ middle))"
    unfolding distinguish_attach[symmetric]
    apply(rule connect_eq_resource_cong)
      apply(rule WT_intro)
     apply(simp del: outs_plus_ℐ add: parallel_converter2_comp1_out attach_compose)
     apply(rule obsf_attach)
       apply(rule pfinite_intro WT_intro)+
    done

  have "advantage ?𝒜 (obsf_resource (sim_inner |⇩= 1⇩C ⊳ ideal)) (obsf_resource middle) ≤ adv1"
    by(rule inner.adv)(rule WT_intro)+
  moreover have "advantage 𝒜 (obsf_resource (sim_outer |⇩= 1⇩C ⊳ middle)) (obsf_resource real) ≤ adv2"
    by(rule outer.adv)(rule WT_intro)+
  ultimately
  show "advantage 𝒜 (obsf_resource (sim_outer ⊙ sim_inner |⇩= 1⇩C ⊳ ideal)) (obsf_resource real) ≤ adv1 + adv2"
    by(auto simp add: advantage_def eq1 eq2 abs_diff_triangle_ineq2)
qed

theorem constructive_security_obsf_lifting:
  assumes sec: "constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common adv"
    and sec2: "exception_ℐ (ℐ_real' ⊕⇩ℐ ℐ_common') ⊢g 𝒜 √ 
    ⟹ constructive_security_sim_obsf real_resource ideal_resource sim ℐ_real ℐ_common (absorb 𝒜 (obsf_converter (w_adv_real |⇩= w_usr))) adv"
    (is "_ ⟹ constructive_security_sim_obsf _ _ _ _ _ ?𝒜 _")
  assumes WT_usr [WT_intro]: "ℐ_common', ℐ_common ⊢⇩C w_usr √"
    and pfinite [pfinite_intro]: "pfinite_converter ℐ_common' ℐ_common w_usr"
    and WT_adv_real [WT_intro]: "ℐ_real', ℐ_real ⊢⇩C w_adv_real √"
    and WT_w_adv_ideal [WT_intro]: "ℐ_ideal', ℐ_ideal ⊢⇩C w_adv_ideal √"
    and WT_adv_ideal_inv [WT_intro]: "ℐ_ideal, ℐ_ideal' ⊢⇩C w_adv_ideal_inv √"
    and ideal_inverse: "ℐ_ideal, ℐ_ideal ⊢⇩C w_adv_ideal_inv ⊙ w_adv_ideal ∼ 1⇩C"
    and pfinite_real [pfinite_intro]: "pfinite_converter ℐ_real' ℐ_real w_adv_real"
    and pfinite_ideal [pfinite_intro]: "pfinite_converter ℐ_ideal ℐ_ideal' w_adv_ideal_inv"
  shows "constructive_security_obsf (w_adv_real |⇩= w_usr ⊳ real_resource) (w_adv_ideal |⇩= w_usr ⊳ ideal_resource) (w_adv_real ⊙ sim ⊙ w_adv_ideal_inv) ℐ_real' ℐ_ideal' ℐ_common' 𝒜 adv"
    (is "constructive_security_obsf ?real ?ideal ?sim ?ℐ_real ?ℐ_ideal _ _ _")
proof
  interpret constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common by fact
  show "ℐ_real' ⊕⇩ℐ ℐ_common' ⊢res ?real √"
    and "ℐ_ideal' ⊕⇩ℐ ℐ_common' ⊢res ?ideal √"
    and "ℐ_real', ℐ_ideal' ⊢⇩C ?sim √" by(rule WT_intro)+
  show "pfinite_converter ℐ_real' ℐ_ideal' ?sim" by(rule pfinite_intro WT_intro)+
  show "0 ≤ adv" by(rule adv_nonneg)

  assume WT_adv [WT_intro]: "exception_ℐ (ℐ_real' ⊕⇩ℐ ℐ_common') ⊢g 𝒜 √"
  then interpret constructive_security_sim_obsf real_resource ideal_resource sim ℐ_real ℐ_common ?𝒜 adv by(rule sec2)

  have *: "advantage ?𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) (obsf_resource real_resource) ≤ adv"
    by(rule adv)(rule WT_intro)+

  have ideal: "connect_obsf ?𝒜 (obsf_resource (sim |⇩= 1⇩C ⊳ ideal_resource)) =
    connect_obsf 𝒜 (obsf_resource (?sim |⇩= 1⇩C ⊳ ?ideal))"
    unfolding distinguish_attach[symmetric]
    apply(rule connect_eq_resource_cong)
      apply(rule WT_intro)
     apply(simp del: outs_plus_ℐ)
     apply(rule eq_resource_on_trans[OF obsf_attach])
        apply(rule pfinite_intro WT_intro)+
     apply(rule obsf_resource_eq_ℐ_cong)
     apply(fold attach_compose)
     apply(unfold comp_converter_parallel2)
     apply(rule eq_ℐ_attach_on')
       apply(rule WT_intro)
      apply(rule parallel_converter2_eq_ℐ_cong)
       apply(unfold comp_converter_assoc)
       apply(rule eq_ℐ_comp_cong)
        apply(rule eq_ℐ_converter_reflI; rule WT_intro)
       apply(rule eq_ℐ_converter_trans[rotated])
        apply(rule eq_ℐ_comp_cong)
         apply(rule eq_ℐ_converter_reflI; rule WT_intro)
        apply(rule ideal_inverse[symmetric])
       apply(unfold comp_converter_id_right comp_converter_id_left)
       apply(rule eq_ℐ_converter_reflI; rule WT_intro)+
     apply simp
    apply(rule WT_intro)+
    done
  have real: "connect_obsf ?𝒜 (obsf_resource real_resource) = connect_obsf 𝒜 (obsf_resource ?real)"
    unfolding distinguish_attach[symmetric]
    apply(rule connect_eq_resource_cong)
      apply(rule WT_intro)
     apply(simp del: outs_plus_ℐ)
     apply(rule obsf_attach)
       apply(rule pfinite_intro WT_intro)+
    done
  show "advantage 𝒜 (obsf_resource ((?sim |⇩= 1⇩C) ⊳ ?ideal)) (obsf_resource ?real) ≤ adv" using *
    unfolding advantage_def ideal[symmetric] real[symmetric] .
qed

corollary constructive_security_obsf_lifting_:
  assumes sec: "constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common (absorb 𝒜 (obsf_converter (w_adv_real |⇩= w_usr))) adv"
  assumes WT_usr [WT_intro]: "ℐ_common', ℐ_common ⊢⇩C w_usr √"
    and pfinite [pfinite_intro]: "pfinite_converter ℐ_common' ℐ_common w_usr"
    and WT_adv_real [WT_intro]: "ℐ_real', ℐ_real ⊢⇩C w_adv_real √"
    and WT_w_adv_ideal [WT_intro]: "ℐ_ideal', ℐ_ideal ⊢⇩C w_adv_ideal √"
    and WT_adv_ideal_inv [WT_intro]: "ℐ_ideal, ℐ_ideal' ⊢⇩C w_adv_ideal_inv √"
    and ideal_inverse: "ℐ_ideal, ℐ_ideal ⊢⇩C w_adv_ideal_inv ⊙ w_adv_ideal ∼ 1⇩C"
    and pfinite_real [pfinite_intro]: "pfinite_converter ℐ_real' ℐ_real w_adv_real"
    and pfinite_ideal [pfinite_intro]: "pfinite_converter ℐ_ideal ℐ_ideal' w_adv_ideal_inv"
  shows "constructive_security_obsf (w_adv_real |⇩= w_usr ⊳ real_resource) (w_adv_ideal |⇩= w_usr ⊳ ideal_resource) (w_adv_real ⊙ sim ⊙ w_adv_ideal_inv) ℐ_real' ℐ_ideal' ℐ_common' 𝒜 adv"
proof -
  interpret constructive_security_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common "absorb 𝒜 (obsf_converter (w_adv_real |⇩= w_usr))" adv by fact
  from constructive_security_aux_obsf constructive_security_sim_obsf assms(2-)
  show ?thesis by(rule constructive_security_obsf_lifting)
qed

theorem constructive_security_obsf_lifting_usr:
  assumes sec: "constructive_security_aux_obsf real_resource ideal_resource sim ℐ_real ℐ_ideal ℐ_common adv"
    and sec2: "exception_ℐ (ℐ_real ⊕⇩ℐ ℐ_common') ⊢g 𝒜 √ 
    ⟹ constructive_security_sim_obsf real_resource ideal_resource sim ℐ_real ℐ_common (absorb 𝒜 (obsf_converter (1⇩C |⇩= conv))) adv"
    and WT_conv [WT_intro]: "ℐ_common', ℐ_common ⊢⇩C conv √"
    and pfinite [pfinite_intro]: "pfinite_converter ℐ_common' ℐ_common conv"
  shows "constructive_security_obsf (1⇩C |⇩= conv ⊳ real_resource) (1⇩C |⇩= conv ⊳ ideal_resource) sim ℐ_real ℐ_ideal ℐ_common' 𝒜 adv"
  by(rule constructive_security_obsf_lifting[OF sec sec2, where ?w_adv_ideal="1⇩C" and ?w_adv_ideal_inv="1⇩C", simplified comp_converter_id_left comp_converter_id_right])
    (rule WT_intro pfinite_intro id_converter_eq_self order_refl | assumption)+

theorem constructive_security_obsf_lifting2:
  assumes sec: "constructive_security_aux_obsf real_resource ideal_resource sim (ℐ_real1 ⊕⇩ℐ ℐ_real2) (ℐ_ideal1 ⊕⇩ℐ ℐ_ideal2) ℐ_common adv"
    and sec2: "exception_ℐ ((ℐ_real1 ⊕⇩ℐ ℐ_real2) ⊕⇩ℐ ℐ_common') ⊢g 𝒜 √ 
    ⟹ constructive_security_sim_obsf real_resource ideal_resource sim (ℐ_real1 ⊕⇩ℐ ℐ_real2) ℐ_common (absorb 𝒜 (obsf_converter ((1⇩C |⇩= 1⇩C) |⇩= conv))) adv"
  assumes WT_conv [WT_intro]: "ℐ_common', ℐ_common ⊢⇩C conv √"
    and pfinite [pfinite_intro]: "pfinite_converter ℐ_common' ℐ_common conv"
  shows "constructive_security_obsf ((1⇩C |⇩= 1⇩C) |⇩= conv ⊳ real_resource) ((1⇩C |⇩= 1⇩C) |⇩= conv ⊳ ideal_resource) sim (ℐ_real1 ⊕⇩ℐ ℐ_real2) (ℐ_ideal1 ⊕⇩ℐ ℐ_ideal2) ℐ_common' 𝒜 adv"
    (is "constructive_security_obsf ?real ?ideal _ ?ℐ_real ?ℐ_ideal _ _ _")
proof -
  interpret constructive_security_aux_obsf real_resource ideal_resource sim "ℐ_real1 ⊕⇩ℐ ℐ_real2" "ℐ_ideal1 ⊕⇩ℐ ℐ_ideal2" ℐ_common adv by fact
  have sim [unfolded comp_converter_id_left]: "ℐ_real1 ⊕⇩ℐ ℐ_real2,ℐ_ideal1 ⊕⇩ℐ ℐ_ideal2 ⊢⇩C (1⇩C |⇩= 1⇩C) ⊙ sim ∼ 1⇩C ⊙ sim"
    by(rule eq_ℐ_comp_cong)(rule parallel_converter2_id_id eq_ℐ_converter_reflI WT_intro)+
  show ?thesis
    apply(rule constructive_security_obsf_sim_cong)
      apply(rule constructive_security_obsf_lifting[OF sec sec2, where ?w_adv_ideal="1⇩C |⇩= 1⇩C" and ?w_adv_ideal_inv="1⇩C", unfolded comp_converter_id_left comp_converter_id_right])
              apply(assumption|rule WT_intro sim pfinite_intro parallel_converter2_id_id)+
    done
qed

theorem constructive_security_obsf_trivial:
  fixes res
  assumes [WT_intro]: "ℐ ⊕⇩ℐ ℐ_common ⊢res res √"
  shows "constructive_security_obsf res res 1⇩C ℐ ℐ ℐ_common 𝒜 0"
proof
  show "ℐ ⊕⇩ℐ ℐ_common ⊢res res √" and "ℐ, ℐ ⊢⇩C 1⇩C √" by(rule WT_intro)+
  show "pfinite_converter ℐ ℐ 1⇩C" by(rule pfinite_intro)

  assume WT [WT_intro]: "exception_ℐ (ℐ ⊕⇩ℐ ℐ_common) ⊢g 𝒜 √"
  have "connect_obsf 𝒜 (obsf_resource (1⇩C |⇩= 1⇩C ⊳ res)) = connect_obsf 𝒜 (obsf_resource (1⇩C ⊳ res))"
    by(rule connect_eq_resource_cong[OF WT])(fastforce intro: WT_intro eq_ℐ_attach_on' obsf_resource_eq_ℐ_cong parallel_converter2_id_id)+
  then show "advantage 𝒜 (obsf_resource (1⇩C |⇩= 1⇩C ⊳ res)) (obsf_resource res) ≤ 0"
    unfolding advantage_def by simp
qed simp

lemma parallel_constructive_security_aux_obsf [locale_witness]:
  assumes "constructive_security_aux_obsf real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 adv1"
  assumes "constructive_security_aux_obsf real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 adv2"
  shows "constructive_security_aux_obsf (parallel_wiring ⊳ real1 ∥ real2) (parallel_wiring ⊳ ideal1 ∥ ideal2) (sim1 |⇩= sim2) 
    (ℐ_real1 ⊕⇩ℐ ℐ_real2) (ℐ_inner1 ⊕⇩ℐ ℐ_inner2) (ℐ_common1 ⊕⇩ℐ ℐ_common2)
    (adv1 + adv2)"
proof
  interpret sec1: constructive_security_aux_obsf real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 adv1 by fact
  interpret sec2: constructive_security_aux_obsf real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 adv2 by fact

  show "(ℐ_real1 ⊕⇩ℐ ℐ_real2) ⊕⇩ℐ (ℐ_common1 ⊕⇩ℐ ℐ_common2) ⊢res parallel_wiring ⊳ real1 ∥ real2 √"
    and "(ℐ_inner1 ⊕⇩ℐ ℐ_inner2) ⊕⇩ℐ (ℐ_common1 ⊕⇩ℐ ℐ_common2) ⊢res parallel_wiring ⊳ ideal1 ∥ ideal2 √"
    and "ℐ_real1 ⊕⇩ℐ ℐ_real2, ℐ_inner1 ⊕⇩ℐ ℐ_inner2 ⊢⇩C sim1 |⇩= sim2 √" by(rule WT_intro)+
  show "pfinite_converter (ℐ_real1 ⊕⇩ℐ ℐ_real2) (ℐ_inner1 ⊕⇩ℐ ℐ_inner2) (sim1 |⇩= sim2)" by(rule pfinite_intro)+
  show "0 ≤ adv1 + adv2" using sec1.adv_nonneg sec2.adv_nonneg by simp
qed

theorem parallel_constructive_security_obsf:
  assumes "constructive_security_obsf real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 (absorb 𝒜 (obsf_converter (parallel_wiring ⊙ parallel_converter 1⇩C (converter_of_resource (sim2 |⇩= 1⇩C ⊳ ideal2))))) adv1"
    (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) 1⇩C))) adv2"
    (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)
    𝒜 (adv1 + adv2)"
proof -
  interpret sec1: constructive_security_obsf real1 ideal1 sim1 ℐ_real1 ℐ_inner1 ℐ_common1 ?𝒜1 adv1 by fact
  interpret sec2: constructive_security_obsf real2 ideal2 sim2 ℐ_real2 ℐ_inner2 ℐ_common2 ?𝒜2 adv2 by fact

  show ?thesis
  proof
    assume WT [WT_intro]: "exception_ℐ ((ℐ_real1 ⊕⇩ℐ ℐ_real2) ⊕⇩ℐ (ℐ_common1 ⊕⇩ℐ ℐ_common2)) ⊢g 𝒜 √"

    have **: "outs_ℐ ((ℐ_real1 ⊕⇩ℐ ℐ_real2) ⊕⇩ℐ (ℐ_common1 ⊕⇩ℐ ℐ_common2)) ⊢⇩R
    ((1⇩C |⇩= sim2) |⇩= 1⇩C |⇩= 1⇩C) ⊙ parallel_wiring ⊳ real1 ∥ ideal2 ∼
    parallel_wiring ⊙ (converter_of_resource real1 |⇩∝ 1⇩C) ⊳ sim2 |⇩= 1⇩C ⊳ ideal2"
      unfolding comp_parallel_wiring
      by(rule eq_resource_on_trans, rule eq_ℐ_attach_on[where conv'="parallel_wiring ⊙ (1⇩C |⇩= sim2 |⇩= 1⇩C)"]
          , (rule WT_intro)+, rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
        (auto simp add: le_ℐ_def attach_compose attach_parallel2 attach_converter_of_resource_conv_parallel_resource
          intro: WT_intro parallel_converter2_eq_ℐ_cong parallel_converter2_id_id eq_ℐ_converter_reflI)

    have ideal2:
      "connect_obsf ?𝒜2 (obsf_resource (sim2 |⇩= 1⇩C ⊳ ideal2)) =
     connect_obsf 𝒜 (obsf_resource ((1⇩C |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 ∥ ideal2))"
      unfolding distinguish_attach[symmetric]
      apply(rule connect_eq_resource_cong)
        apply(rule WT_intro)
       apply(simp del: outs_plus_ℐ)
       apply(rule eq_resource_on_trans[OF obsf_attach])
          apply(rule pfinite_intro WT_intro)+
       apply(rule obsf_resource_eq_ℐ_cong)
       apply(rule eq_resource_on_sym)
       apply(subst attach_compose[symmetric])
       apply(rule **)
      apply(rule WT_intro)+
      done

    have real2: "connect_obsf ?𝒜2 (obsf_resource real2) = connect_obsf 𝒜 (obsf_resource (parallel_wiring ⊳ real1 ∥ real2))"
      unfolding distinguish_attach[symmetric]
      apply(rule connect_eq_resource_cong)
        apply(rule WT_intro)
       apply(simp del: outs_plus_ℐ)
       apply(rule eq_resource_on_trans[OF obsf_attach])
          apply(rule pfinite_intro WT_intro)+
       apply(rule obsf_resource_eq_ℐ_cong)
       apply(rule eq_resource_on_sym)
      by(simp add: attach_compose attach_converter_of_resource_conv_parallel_resource)(rule WT_intro)+

    have adv2: "advantage 𝒜
     (obsf_resource ((1⇩C |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 ∥ ideal2))
     (obsf_resource (parallel_wiring ⊳ real1 ∥ real2)) ≤ adv2"
      unfolding advantage_def ideal2[symmetric] real2[symmetric] by(rule sec2.adv[unfolded advantage_def])(rule WT_intro)+

    have ideal1: 
      "connect_obsf ?𝒜1 (obsf_resource (sim1 |⇩= 1⇩C ⊳ ideal1)) = 
     connect_obsf 𝒜 (obsf_resource ((sim1 |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ ideal1 ∥ ideal2))"
    proof -
      have *:"((outs_ℐ ℐ_real1 <+> outs_ℐ ℐ_real2) <+> outs_ℐ ℐ_common1 <+> outs_ℐ ℐ_common2) ⊢⇩R
    (sim1 |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ ideal1 ∥ ideal2 ∼
    parallel_wiring ⊙ (1⇩C |⇩∝ converter_of_resource (sim2 |⇩= 1⇩C ⊳ ideal2)) ⊳ sim1 |⇩= 1⇩C ⊳ ideal1"
        by(auto simp add: le_ℐ_def comp_parallel_wiring' attach_compose attach_parallel2 attach_converter_of_resource_conv_parallel_resource2 intro: WT_intro)
      show ?thesis
        unfolding distinguish_attach[symmetric] 
        apply(rule connect_eq_resource_cong)
          apply(rule WT_intro)
         apply(simp del: outs_plus_ℐ)
         apply(rule eq_resource_on_trans[OF obsf_attach])
            apply(rule pfinite_intro WT_intro)+
         apply(rule obsf_resource_eq_ℐ_cong)
         apply(rule eq_resource_on_sym)
        by(simp add: *, (rule WT_intro)+)
    qed

    have real1: "connect_obsf ?𝒜1 (obsf_resource real1) = connect_obsf 𝒜 (obsf_resource ((1⇩C |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 ∥ ideal2))"
    proof -
      have *: "outs_ℐ ((ℐ_real1 ⊕⇩ℐ ℐ_real2) ⊕⇩ℐ (ℐ_common1 ⊕⇩ℐ ℐ_common2)) ⊢⇩R
    parallel_wiring ⊙ ((1⇩C |⇩= 1⇩C) |⇩= sim2 |⇩= 1⇩C) ⊳ real1 ∥ ideal2 ∼
    parallel_wiring ⊙ (1⇩C |⇩∝ converter_of_resource (sim2 |⇩= 1⇩C ⊳ ideal2 )) ⊳ real1"
        by(rule eq_resource_on_trans, rule eq_ℐ_attach_on[where conv'="parallel_wiring ⊙ (1⇩C |⇩= sim2 |⇩= 1⇩C)"]
            , (rule WT_intro)+, rule eq_ℐ_comp_cong, rule eq_ℐ_converter_mono)
          (auto simp add: le_ℐ_def attach_compose attach_converter_of_resource_conv_parallel_resource2 attach_parallel2 
            intro: WT_intro parallel_converter2_eq_ℐ_cong parallel_converter2_id_id eq_ℐ_converter_reflI)

      show ?thesis
        unfolding distinguish_attach[symmetric] 
        apply(rule connect_eq_resource_cong)
          apply(rule WT_intro)
         apply(simp del: outs_plus_ℐ)
         apply(rule eq_resource_on_trans[OF obsf_attach])
            apply(rule pfinite_intro WT_intro)+
         apply(rule obsf_resource_eq_ℐ_cong)
         apply(rule eq_resource_on_sym)
         apply(fold attach_compose)
         apply(subst comp_parallel_wiring)
         apply(rule *)
        apply(rule WT_intro)+
        done
    qed

    have adv1: "advantage 𝒜 
     (obsf_resource ((sim1 |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ ideal1 ∥ ideal2))
     (obsf_resource ((1⇩C |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ real1 ∥ ideal2)) ≤ adv1"
      unfolding advantage_def ideal1[symmetric] real1[symmetric] by(rule sec1.adv[unfolded advantage_def])(rule WT_intro)+

    from adv1 adv2 show "advantage 𝒜 (obsf_resource ((sim1 |⇩= sim2) |⇩= (1⇩C |⇩= 1⇩C) ⊳ parallel_wiring ⊳ ideal1 ∥ ideal2))
         (obsf_resource (parallel_wiring ⊳ real1 ∥ real2)) ≤ adv1 + adv2"
      by(auto simp add: advantage_def)
  qed
qed

theorem parallel_constructive_security_obsf_fuse:
  assumes 1: "constructive_security_obsf real1 ideal1 sim1 (ℐ_real1_core ⊕⇩ℐ ℐ_real1_rest) (ℐ_ideal1_core ⊕⇩ℐ ℐ_ideal1_rest) (ℐ_common1_core ⊕⇩ℐ ℐ_common1_rest) (absorb 𝒜 (obsf_converter (fused_wiring ⊙ parallel_converter 1⇩C (converter_of_resource (sim2 |⇩= 1⇩C ⊳ ideal2))))) adv1"
    (is "constructive_security_obsf _ _ _ ?ℐ_real1 ?ℐ_ideal1 ?ℐ_common1 ?𝒜1 _")
  assumes 2: "constructive_security_obsf real2 ideal2 sim2 (ℐ_real2_core ⊕⇩ℐ ℐ_real2_rest) (ℐ_ideal2_core ⊕⇩ℐ ℐ_ideal2_rest) (ℐ_common2_core ⊕⇩ℐ ℐ_common2_rest) (absorb 𝒜 (obsf_converter (fused_wiring ⊙ parallel_converter (converter_of_resource real1) 1⇩C))) adv2"
    (is "constructive_security_obsf _ _ _ ?ℐ_real2 ?ℐ_ideal2 ?ℐ_common2 ?𝒜2 _")
  shows "constructive_security_obsf (fused_wiring ⊳ real1 ∥ real2) (fused_wiring ⊳ ideal1 ∥ ideal2) 
    (parallel_wiring ⊙ (sim1 |⇩= sim2) ⊙ parallel_wiring)
    ((ℐ_real1_core ⊕⇩ℐ ℐ_real2_core) ⊕⇩ℐ (ℐ_real1_rest ⊕⇩ℐ ℐ_real2_rest)) 
    ((ℐ_ideal1_core ⊕⇩ℐ ℐ_ideal2_core) ⊕⇩ℐ (ℐ_ideal1_rest ⊕⇩ℐ ℐ_ideal2_rest))
    ((ℐ_common1_core ⊕⇩ℐ ℐ_common2_core) ⊕⇩ℐ (ℐ_common1_rest ⊕⇩ℐ ℐ_common2_rest))
    𝒜 (adv1 + adv2)"
proof -
  interpret sec1: constructive_security_obsf real1 ideal1 sim1 ?ℐ_real1 ?ℐ_ideal1 ?ℐ_common1 ?𝒜1 adv1 by fact
  interpret sec2: constructive_security_obsf real2 ideal2 sim2 ?ℐ_real2 ?ℐ_ideal2 ?ℐ_common2 ?𝒜2 adv2 by fact

  have aux1: "constructive_security_aux_obsf real1 ideal1 sim1 ?ℐ_real1 ?ℐ_ideal1 ?ℐ_common1 adv1" ..
  have aux2: "constructive_security_aux_obsf real2 ideal2 sim2 ?ℐ_real2 ?ℐ_ideal2 ?ℐ_common2 adv2" ..

  have sim: "constructive_security_sim_obsf (parallel_wiring ⊳ real1 ∥ real2) (parallel_wiring ⊳ ideal1 ∥ ideal2) (sim1 |⇩= sim2)
      (?ℐ_real1 ⊕⇩ℐ ?ℐ_real2) (?ℐ_common1 ⊕⇩ℐ ?ℐ_common2)
      (absorb 𝒜 (obsf_converter (parallel_wiring |⇩= parallel_wiring)))
      (adv1 + adv2)"
    if [WT_intro]: "exception_ℐ (((ℐ_real1_core ⊕⇩ℐ ℐ_real2_core) ⊕⇩ℐ (ℐ_real1_rest ⊕⇩ℐ ℐ_real2_rest)) ⊕⇩ℐ ((ℐ_common1_core ⊕⇩ℐ ℐ_common2_core) ⊕⇩ℐ (ℐ_common1_rest ⊕⇩ℐ ℐ_common2_rest))) ⊢g 𝒜 √"
  proof -
    interpret constructive_security_obsf 
      "parallel_wiring ⊳ real1 ∥ real2"
      "parallel_wiring ⊳ ideal1 ∥ ideal2"
      "sim1 |⇩= sim2"
      "?ℐ_real1 ⊕⇩ℐ ?ℐ_real2" "?ℐ_ideal1 ⊕⇩ℐ ?ℐ_ideal2" "?ℐ_common1 ⊕⇩ℐ ?ℐ_common2"
      "absorb 𝒜 (obsf_converter (parallel_wiring |⇩= parallel_wiring))"
      "adv1 + adv2"
      apply(rule parallel_constructive_security_obsf)
       apply(fold absorb_comp_converter)
       apply(rule constructive_security_obsf_absorb_cong[OF 1])
          apply(rule WT_intro)+
       apply(unfold fused_wiring_def comp_converter_assoc)
       apply(rule obsf_comp_converter)
         apply(rule WT_intro pfinite_intro)+
      apply(rule constructive_security_obsf_absorb_cong[OF 2])
         apply(rule WT_intro)+
      apply(subst fused_wiring_def)                                               
      apply(unfold comp_converter_assoc)
      apply(rule obsf_comp_converter)
        apply(rule WT_intro pfinite_intro wiring_intro parallel_wiring_inverse)+
      done
    show ?thesis ..
  qed
  show ?thesis
    unfolding fused_wiring_def attach_compose
    apply(rule constructive_security_obsf_lifting[where w_adv_ideal_inv=parallel_wiring])
             apply(rule parallel_constructive_security_aux_obsf[OF aux1 aux2])
            apply(erule sim)
           apply(rule WT_intro pfinite_intro parallel_wiring_inverse)+
    done
qed

end