Skip to content

Instantly share code, notes, and snippets.

@asifmallik

asifmallik/CDHtoDDH.ec

Created June 16, 2019 14:31
Show Gist options
  • Save asifmallik/630d68790813075d76e2871dad297faf to your computer and use it in GitHub Desktop.
Save asifmallik/630d68790813075d76e2871dad297faf to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment