https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
elgamal.ec
(* -------------------------------------------------------------------- *)
require import AllCore Int Real Distr DBool.
require (*--*) DiffieHellman PKE_CPA.
(* ---------------- Sane Default Behaviours --------------------------- *)
pragma -oldip.
pragma +implicits.
(* ---------------------- Let's Get Started --------------------------- *)
(** Assumption: set DDH *)
(*** WARNING: DiffieHellman is really out of date ***)
clone import DiffieHellman as DH.
import DDH FDistr.
(** Construction: a PKE **)
type pkey = group.
type skey = F.t.
type ptxt = group.
type ctxt = group * group.
clone import PKE_CPA as PKE with
type pkey <- pkey,
type skey <- skey,
type ptxt <- ptxt,
type ctxt <- ctxt.
(** Concrete Construction: Hashed ElGammal **)
module ElGamal : Scheme = {
proc kg(): pkey * skey = {
var sk;
sk <$ dt;
return (g ^ sk, sk);
}
proc enc(pk:pkey, m:ptxt): ctxt = {
var y;
y <$ dt;
return (g ^ y, pk ^ y * m);
}
proc dec(sk:skey, c:ctxt): ptxt option = {
var gy, gm;
(gy, gm) <- c;
return Some (gm * gy^(-sk));
}
}.
(** Reduction: from a PKE adversary, construct a DDH adversary *)
module DDHAdv (A:Adversary) = {
proc guess (gx, gy, gz) : bool = {
var m0, m1, b, b';
(m0, m1) <- A.choose(gx);
b <$ {0,1};
b' <@ A.guess(gy, gz * (b?m1:m0));
return b' = b;
}
}.
(** We now prove that, for all adversary A, we have:
`| Pr[CPA(ElGamal,A).main() @ &m : res] - 1%r/2%r |
= `| Pr[DDH0(DDHAdv(A)).main() @ &m : res]
- Pr[DDH1(DDHAdv(A)).main() @ &m : res] |. **)
section Security.
declare module A:Adversary.
axiom Ac_ll: islossless A.choose.
axiom Ag_ll: islossless A.guess.
local lemma cpa_ddh0 &m:
Pr[CPA(ElGamal,A).main() @ &m : res] =
Pr[DDH0(DDHAdv(A)).main() @ &m : res].
proof.
byequiv=> //; proc; inline *.
swap{1} 7 -5.
auto; call (_:true).
auto; call (_:true).
by auto=> /> sk _ y _ r b _; rewrite pow_pow.
qed.
local module Gb = {
proc main () : bool = {
var x, y, z, m0, m1, b, b';
x <$ FDistr.dt;
y <$ FDistr.dt;
(m0,m1) <@ A.choose(g^x);
z <$ FDistr.dt;
b' <@ A.guess(g^y, g^z);
b <$ {0,1};
return b' = b;
}
}.
local lemma ddh1_gb &m:
Pr[DDH1(DDHAdv(A)).main() @ &m : res] =
Pr[Gb.main() @ &m : res].
proof.
byequiv=> //; proc; inline *.
swap{1} 3 2; swap{1} [5..6] 2; swap{2} 6 -2.
auto; call (_:true); wp.
rnd (fun z, z + log (if b then m1 else m0){2})
(fun z, z - log (if b then m1 else m0){2}).
auto; call (_:true).
auto=> /> x _ y _ [m0 m1] b _; progress.
+ by algebra.
+ exact/FDistr.dt_funi.
+ exact/FDistr.dt_fu.
+ by algebra.
+ by algebra.
qed.
local lemma Gb_half &m:
Pr[Gb.main()@ &m : res] = 1%r/2%r.
proof.
byphoare=> //; proc.
rnd (pred1 b')=> //=.
conseq (: _ ==> true).
+ by move=> /> b; rewrite dbool1E pred1E.
call Ag_ll.
auto; call Ac_ll.
by auto=> />; exact/dt_ll.
qed.
lemma conclusion &m :
`| Pr[CPA(ElGamal,A).main() @ &m : res] - 1%r/2%r | =
`| Pr[DDH0(DDHAdv(A)).main() @ &m : res] -
Pr[DDH1(DDHAdv(A)).main() @ &m : res] |.
proof.
by rewrite (cpa_ddh0 &m) (ddh1_gb &m) (Gb_half &m).
qed.
end section Security.
print conclusion.