Revision 38fb166e8c1dfe73ca59bbe84d78ded157f94ec4 authored by Pierre-Yves Strub on 05 September 2022, 08:14:39 UTC, committed by Pierre-Yves Strub on 05 September 2022, 08:25:14 UTC
1 parent f8c2cac
PRG.eca
(*** 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]| **)
Computing file changes ...