https://github.com/EasyCrypt/easycrypt
Tip revision: ea6c7da4938617fceaa87cc31d88233314482d92 authored by Pierre-Yves Strub on 16 April 2020, 13:06:48 UTC
Move "monogenous" to Group.
Move "monogenous" to Group.
Tip revision: ea6c7da
DLog.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2016--2017 - Roberto Metere (r.metere2@ncl.ac.uk)
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* 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.