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
      (1C |= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |= 1C 
       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))
      ((1C 
        (parallel_wiring  ((let sim = CNV dh.sim_callee None in (sim |= 1C)  lassocrC) |= 1C)  parallel_wiring) 
        1C) 
       (otp.sim |= 1C))
      ((((ℐ_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 (1C |= wiring_c1r22_c1r22 (CNV otp.enc_callee ()) (CNV otp.dec_callee ()) |= 1C)))
                    (obsf_converter
                      (fused_wiring  (1C | converter_of_resource (1C |= 1C  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="1C" and w_adv_ideal_inv="1C"])
          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