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
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]| **)