CDHtoDDH.ec

require import AllCore Int Real Distr DBool.
require DiffieHellman.

  pragma -oldip.
  pragma +implicits.

clone import DiffieHellman as DH.


module type Adversary = {
  proc solve(gx:group, gy:group): group
}.

module DDH_from_CDH (B:DH.CDH.Adversary) : DH.DDH.Adversary  = {
  proc guess (gx gy gz: group) : bool = {
    var r;
    r = B.solve(gx, gy);
    return (r = gz);
  }
}.

section Reduction.

declare module A: DH.CDH.Adversary.
axiom A_ll: islossless A.solve.

lemma partReduction &m : Pr[DH.CDH.CDH(A).main() @ &m: res] = Pr[DH.DDH.DDH0(DDH_from_CDH(A)).main() @ &m : res]. proof. byequiv=> //; proc; inline *. auto. call(_: true). auto. qed.  

lemma partReduction2 &m : Pr[DH.DDH.DDH1(DDH_from_CDH(A)).main() @ &m : res] = 1%r/(F.q)%r. proof. byphoare; first last. trivial. trivial. proc; inline *. auto. swap 6 1. auto. swap 3 3. rnd. auto. call(_: true). by apply A_ll.
auto. move=>?. simplify. split. apply FDistr.dt_ll. move => ll s x. split. move=> l;split. by apply ll. move => ll2; move=> {ll2}. move => t. move=> r. split. move => s2 s3. have h := mu_eq FDistr.dt (fun (x0 : t) => s3 = g ^ x0) (pred1 (log s3)). rewrite  /(==)  in  h. by smt. by smt. by smt. qed.
    
  lemma Reduction &m : `|Pr[DH.CDH.CDH(A).main() @ &m: res] - 1%r/q%r | = `| Pr[DH.DDH.DDH0(DDH_from_CDH(A)).main() @ &m: res] - Pr[DH.DDH.DDH1(DDH_from_CDH(A)).main() @ &m: res] |. 
    proof. by smt. qed.