Pseudorandom Generators (PRGs)

This file defines pseudorandom generators and their security game.

A PRG stretches a short random seed into a longer pseudorandom output. Security means no efficient adversary can distinguish gen(s) (for a random seed s) from a truly random output r.

Main Definitions

• PRGScheme S R — a PRG with seed space S and output space R.
• PRGAdversary R — a distinguisher receiving a single value in R.
• prgRealExp — the real experiment (adversary sees gen(s) for random s).
• prgIdealExp — the ideal experiment (adversary sees random r).
• prgAdvantage — distinguishing advantage.

structure PRGScheme (S R : Type) : Type

A pseudorandom generator with seed space S and output space R. The generator is a deterministic function; security comes from the seed being sampled uniformly.

• gen : S → R

def PRGScheme.PRGAdversary (R : Type) : Type

A PRG adversary receives a single value and guesses whether it was generated by the PRG or sampled uniformly.

def PRGScheme.prgRealExp {S R : Type} [SampleableType S] (prg : PRGScheme S R) (adversary : PRGAdversary R) : ProbComp Bool

Real PRG experiment: sample a random seed and let the adversary see the PRG output.

def PRGScheme.prgIdealExp {R : Type} [SampleableType R] (adversary : PRGAdversary R) : ProbComp Bool

Ideal PRG experiment: let the adversary see a uniformly random value.

noncomputable def PRGScheme.prgAdvantage {S R : Type} [SampleableType S] [SampleableType R] (prg : PRGScheme S R) (adversary : PRGAdversary R) : ℝ

PRG advantage: how well the adversary distinguishes PRG output from random.