https://github.com/EasyCrypt/easycrypt
Tip revision: 895e467d1beefdebcaa7bcf3306604947f525637 authored by Benjamin Gregoire on 25 January 2023, 14:28:17 UTC
cleanup
cleanup
Tip revision: 895e467
DLog.ec
(* A formalisation of the discrete logarithm assumption. *)
require import CyclicGroup.
require import Real.
theory DLog.
(* This is the standard definition of discrete logarithm experiment *)
module type StdAdversary = {
proc guess(h : group) : F.t
}.
module DLogStdExperiment(A:StdAdversary) = {
proc main () : bool = {
var x, x';
x <$ FDistr.dt;
x' <@ A.guess(g^x);
return (x' = x);
}
}.
(*
This is a modified definition in which the adversary may fail.
In comparison, the standard adversary always tries to provide an answer,
which may be succesful with probability 1/q, where q grows exponentially
in the security parameter.
*)
module type Adversary = {
proc guess(h : group) : F.t option
}.
module DLogExperiment(A:Adversary) = {
proc main () : bool = {
var x, x';
x <$ FDistr.dt;
x' <@ A.guess(g^x);
return (x' = Some x);
}
}.
end DLog.
(*
Reduction of the experiment admitting failure to the standard DLog experiment.
*)
section DLogSecurity.
declare module L <: DLog.Adversary.
module StdRedAdversary(L:DLog.Adversary) = {
proc guess(h: group) : F.t = {
var lx, x;
lx <@ L.guess(h);
if (lx = None)
x <$ FDistr.dt; (* the best if L gave up *)
else
x <- oget lx;
return x;
}
}.
lemma dlog_standard_reduction &m:
Pr[DLog.DLogExperiment(L).main() @ &m : res] <=
Pr[DLog.DLogStdExperiment(StdRedAdversary(L)).main() @ &m : res].
proof.
byequiv => //; proc; inline*.
wp; seq 2 3: (x'{1} = lx{2} /\ x{1} = x{2}).
+ by call (_: true); auto.
if{2} => //; last by auto.
auto => />; apply FDistr.dt_ll.
qed.
end section DLogSecurity.