Theory DH_Ext

subsection ‹DHH Extension›

text ‹We define a variant of the DDH assumption and show it is as hard as the original DDH assumption.›

theory DH_Ext imports
  Game_Based_Crypto.Diffie_Hellman
  Cyclic_Group_Ext
begin

context ddh begin

definition DDH0 :: "'grp adversary ⇒ bool spmf"
  where "DDH0 𝒜 = do {
    s ← sample_uniform (order 𝒢);
    r ← sample_uniform (order 𝒢);
    let h = ❙g [^] s;
    𝒜 h (❙g [^] r) (h [^] r)}"

definition DDH1 :: "'grp adversary ⇒ bool spmf"
  where "DDH1 𝒜 = do {
    s ← sample_uniform (order 𝒢);
    r ← sample_uniform (order 𝒢);
    let h = ❙g [^] s;
    𝒜 h (❙g [^] r) ((h [^] r) ⊗ ❙g)}"

definition DDH_advantage :: "'grp adversary ⇒ real"
  where "DDH_advantage 𝒜 = ¦spmf (DDH0 𝒜) True - spmf (DDH1 𝒜) True¦"

definition DDH_𝒜' :: "'grp adversary ⇒ 'grp ⇒ 'grp ⇒ 'grp ⇒ bool spmf"
  where "DDH_𝒜' D_ddh a b c = D_ddh a b (c ⊗ ❙g)"

end 

locale ddh_ext = ddh + cyclic_group 𝒢
begin

lemma DDH0_eq_ddh_0: "ddh.DDH0 𝒢 𝒜 = ddh.ddh_0 𝒢 𝒜"
  by(simp add: ddh.DDH0_def Let_def monoid.nat_pow_pow ddh.ddh_0_def) 

lemma DDH_bound1: "¦spmf (ddh.DDH0 𝒢 𝒜) True - spmf (ddh.DDH1 𝒢 𝒜) True¦ 
                        ≤ ¦spmf (ddh.ddh_0 𝒢 𝒜) True - spmf (ddh.ddh_1 𝒢 𝒜) True¦ 
                              + ¦spmf (ddh.ddh_1 𝒢 𝒜) True - spmf (ddh.DDH1 𝒢 𝒜) True¦"
  by (simp add: abs_diff_triangle_ineq2 DDH0_eq_ddh_0)

lemma DDH_bound2: 
  shows "¦spmf (ddh.DDH0 𝒢 𝒜) True - spmf (ddh.DDH1 𝒢 𝒜) True¦ 
               ≤ ddh.advantage 𝒢 𝒜 + ¦spmf (ddh.ddh_1 𝒢 𝒜) True - spmf (ddh.DDH1 𝒢 𝒜) True¦"
  using advantage_def DDH_bound1 by simp

lemma rewrite: 
  shows "(sample_uniform (order 𝒢) ⤜ (λx. sample_uniform (order 𝒢) 
            ⤜ (λy. sample_uniform (order 𝒢) ⤜ (λz. 𝒜 (❙g [^] x) (❙g [^] y) (❙g [^] z ⊗ ❙g))))) 
              = (sample_uniform (order 𝒢) ⤜ (λx. sample_uniform (order 𝒢) 
                ⤜ (λy. sample_uniform (order 𝒢) ⤜ (λz. 𝒜 (❙g [^] x) (❙g [^] y) (❙g [^] z)))))"
(is "?lhs = ?rhs")
proof-
  have "?lhs = do {
   x ← sample_uniform (order 𝒢);
   y ← sample_uniform (order 𝒢);
   c ← map_spmf (λ z. ❙g [^] z ⊗ ❙g) (sample_uniform (order 𝒢));
   𝒜 (❙g [^] x) (❙g [^] y) c}" 
    by(simp add: o_def bind_map_spmf Let_def)
  also have "... = do {
   x ← sample_uniform (order 𝒢);
   y ← sample_uniform (order 𝒢);
   c ← map_spmf (λx. ❙g [^] x) (sample_uniform (order 𝒢));
   𝒜 (❙g [^] x) (❙g [^] y) c}" 
    by(simp add: sample_uniform_one_time_pad)
  ultimately show ?thesis 
    by(simp add: Let_def bind_map_spmf o_def)
qed

lemma DDH_𝒜'_bound: "ddh.advantage 𝒢 (ddh.DDH_𝒜' 𝒢 𝒜) = ¦spmf (ddh.ddh_1 𝒢 𝒜) True - spmf (ddh.DDH1 𝒢 𝒜) True¦"
  unfolding ddh.advantage_def ddh.ddh_1_def ddh.DDH1_def Let_def ddh.DDH_𝒜'_def ddh.ddh_0_def 
  by (simp add: rewrite abs_minus_commute nat_pow_pow)

lemma DDH_advantage_bound: "ddh.DDH_advantage 𝒢 𝒜 ≤ ddh.advantage 𝒢 𝒜 + ddh.advantage 𝒢 (ddh.DDH_𝒜' 𝒢 𝒜)"
  using DDH_bound2 DDH_𝒜'_bound DDH_advantage_def by simp

end 

end