https://github.com/EasyCrypt/easycrypt
Tip revision: 67e98eaa3714519dfbb21f454f478fa3bb68fdf2 authored by Pierre-Yves Strub on 30 April 2021, 14:14:14 UTC
Merge branch '1.0' into 1.0-preview
Merge branch '1.0' into 1.0-preview
Tip revision: 67e98ea
elgamal.ec
(* -------------------------------------------------------------------- *)
require import AllCore Int Real Distr DBool.
require (*--*) DiffieHellman PKE_CPA.
(* ---------------- Sane Default Behaviours --------------------------- *)
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).
by auto; progress; 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.
islossless;[ apply Ag_ll | apply Ac_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.