https://github.com/EasyCrypt/easycrypt
Tip revision: 374dae60b90d55b70e41805c88b33b26faaa455d authored by Pierre-Yves Strub on 12 October 2021, 13:09:21 UTC
parser: fix precedence issue
parser: fix precedence issue
Tip revision: 374dae6
PRG.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(*** A formalization of pseudo-random generators **)
(** A stateful random generator for type output is a pair of
algorithms init and next as specified below **)
type output.
module type RG = {
proc init(): unit
proc next(): output
}.
(** PRG-security is expressed w.r.t. an arbitrary distribution dout on
type output (usually the uniform distribution on the full type):
no adversary should be able to distinguish between a sequence of
outputs produced by the SRG and a sequence of samples in dout **)
op dout:output distr.
module type RGA = { proc next(): output }.
module type Distinguisher(G:RGA) = { proc distinguish(): bool }.
module IND(G:RG,D:Distinguisher) = {
module D = D(G)
proc main(): bool = {
var b;
G.init();
b <@ D.distinguish();
return b;
}
}.
module PRGi:RG,RGA = {
proc init(): unit = { }
proc next(): output = { var r; r <$ dout; return r; }
}.
(** Advantage of a distinguisher against a PRG G:
Adv^PRG_G(&m,D) = `|Pr[IND(G,D) @ &m: res] - Pr[IND(PRGi,D) @ &m: res]| **)