Theory DH_OTP

theory DH_OTP imports
  One_Time_Pad
  Diffie_Hellman_CC
begin

text ‹
  We need both a group structure and a boolean algebra.
  Unfortunately, records allow only one extension slot, so we can't have just a single
  structure with both operations.
›

context diffie_hellman begin

lemma WT_ideal_rest [WT_intro]:
  assumes WT_auth1_rest [WT_intro]: "WT_rest ℐ_adv_rest1 ℐ_usr_rest1 I_auth1_rest auth1_rest"
    and WT_auth2_rest [WT_intro]: "WT_rest ℐ_adv_rest2 ℐ_usr_rest2 I_auth2_rest auth2_rest"
  shows "WT_rest (ℐ_full ⊕⇩ℐ (ℐ_adv_rest1 ⊕⇩ℐ ℐ_adv_rest2)) ((ℐ_full ⊕⇩ℐ ℐ_full) ⊕⇩ℐ (ℐ_usr_rest1 ⊕⇩ℐ ℐ_usr_rest2))
     (λ(_, s). pred_prod I_auth1_rest I_auth2_rest s) (ideal_rest auth1_rest auth2_rest)"
  apply(rule WT_rest.intros)
  subgoal
    by(auto 4 4 split: sum.splits simp add: translate_eoracle_def parallel_eoracle_def dest: assms[THEN WT_restD_rfunc_adv])
  subgoal
    apply(auto 4 4 split: sum.splits simp add: translate_eoracle_def parallel_eoracle_def plus_eoracle_def dest: assms[THEN WT_restD_rfunc_usr])
    apply(simp add: map_sum_def split: sum.splits)
    done
  subgoal by(simp add: assms[THEN WT_restD_rinit])
done

end


locale dh_otp = dh: diffie_hellman 𝒢 + otp: one_time_pad ℒ
  for 𝒢 :: "'grp cyclic_group"
    and ℒ :: "'grp boolean_algebra" +
  assumes carrier_𝒢_ℒ: "carrier 𝒢 = carrier ℒ"
begin

theorem secure:
  assumes "WT_rest ℐ_adv_resta ℐ_usr_resta I_auth_rest auth_rest"
    and "WT_rest ℐ_adv_rest1 ℐ_usr_rest1 I_auth1_rest auth1_rest"
    and "WT_rest ℐ_adv_rest2 ℐ_usr_rest2 I_auth2_rest auth2_rest"
  shows
    "constructive_security_obsf
      (1⇩C |⇩= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |⇩= 1⇩C ⊳
       fused_wiring ⊳ diffie_hellman.real_resource 𝒢 auth1_rest auth2_rest ∥ dh.auth.resource auth_rest)
      (otp.sec.resource (otp.ideal_rest (dh.ideal_rest auth1_rest auth2_rest) auth_rest))
      ((1⇩C ⊙
        (parallel_wiring ⊙ ((let sim = CNV dh.sim_callee None in (sim |⇩= 1⇩C) ⊙ lassocr⇩C) |⇩= 1⇩C) ⊙ parallel_wiring) ⊙
        1⇩C) ⊙
       (otp.sim |⇩= 1⇩C))
      ((((ℐ_full ⊕⇩ℐ (ℐ_full ⊕⇩ℐ ℐ_uniform (otp.sec.Inp_Fedit ` carrier 𝒢) UNIV)) ⊕⇩ℐ
         (ℐ_full ⊕⇩ℐ (ℐ_full ⊕⇩ℐ ℐ_uniform (otp.sec.Inp_Fedit ` carrier 𝒢) UNIV))) ⊕⇩ℐ
        (ℐ_full ⊕⇩ℐ (ℐ_full ⊕⇩ℐ ℐ_uniform (otp.sec.Inp_Fedit ` carrier ℒ) UNIV))) ⊕⇩ℐ
       ((ℐ_adv_rest1 ⊕⇩ℐ ℐ_adv_rest2) ⊕⇩ℐ ℐ_adv_resta))
      ((ℐ_full ⊕⇩ℐ (ℐ_full ⊕⇩ℐ ℐ_uniform (otp.sec.Inp_Fedit ` carrier ℒ) UNIV)) ⊕⇩ℐ
       ((ℐ_full ⊕⇩ℐ (ℐ_adv_rest1 ⊕⇩ℐ ℐ_adv_rest2)) ⊕⇩ℐ ℐ_adv_resta))
      ((ℐ_uniform (otp.sec.Inp_Send ` carrier ℒ) UNIV ⊕⇩ℐ ℐ_uniform UNIV (otp.sec.Out_Recv ` carrier ℒ)) ⊕⇩ℐ
       (((ℐ_full ⊕⇩ℐ ℐ_full) ⊕⇩ℐ (ℐ_usr_rest1 ⊕⇩ℐ ℐ_usr_rest2)) ⊕⇩ℐ ℐ_usr_resta))
      𝒜 (0 + (ddh.advantage 𝒢
                (diffie_hellman.DH_adversary 𝒢 auth1_rest auth2_rest
                  (absorb
                    (absorb 𝒜
                      (obsf_converter (1⇩C |⇩= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |⇩= 1⇩C)))
                    (obsf_converter
                      (fused_wiring ⊙ (1⇩C |⇩∝ converter_of_resource (1⇩C |⇩= 1⇩C ⊳ dh.auth.resource auth_rest)))))) +
               0))"
  using assms apply -
  apply(rule constructive_security_obsf_composability)
   apply(rule otp.secure)
    apply(rule WT_intro, assumption+)
  unfolding otp.real_resource_def attach_c1f22_c1f22_def[abs_def] attach_compose
  apply(rule constructive_security_obsf_lifting_[where w_adv_real="1⇩C" and w_adv_ideal_inv="1⇩C"])
          apply(rule parallel_constructive_security_obsf_fuse)
           apply(fold carrier_𝒢_ℒ)[1]
           apply(rule dh.secure, assumption, assumption, rule constructive_security_obsf_trivial)
          defer
          defer
          defer
          apply(rule WT_intro)+
       apply(simp add: comp_converter_id_left)
       apply(rule parallel_converter2_id_id pfinite_intro wiring_intro)+
    apply(rule WT_intro|assumption)+
    apply simp
   apply(unfold wiring_c1r22_c1r22_def)
   apply(rule WT_intro)+
    apply(fold carrier_𝒢_ℒ)[1]
    apply(rule WT_intro)+

  apply(rule pfinite_intro)
   apply(rule pfinite_intro)
      apply(rule pfinite_intro)
       apply(rule pfinite_intro)
      apply(rule pfinite_intro)
     apply(unfold carrier_𝒢_ℒ)
     apply(rule pfinite_intro)
    apply(rule WT_intro)+
  apply(rule pfinite_intro)
  done

end

end