Bijection PRG: Perfect Security

A pseudorandom generator that is a bijection from seeds to outputs has perfect security. Following Rosulek, The Joy of Cryptography, §5 (pseudorandom generators).

If the stretch map s ↦ stretch s is a bijection from the seed space onto the output space, then over a uniform seed the generator output is itself uniform on the output space. Hence the PRG real game (stretch a uniform seed) and the PRG ideal game (a fresh uniform output) are perfectly indistinguishable: the PRG advantage of every adversary is exactly 0.

Overview

This mirrors the one-time-pad and bijection-PRF arguments (CatCrypt.Examples.OTP, CatCrypt.Examples.PRF): the security proof is the bijection-coupling technique. liftR_uniform_bij couples the uniform seed with the uniform output through the bijection bij : Seed ≃ Output; liftR_bind/liftR_pure push the coupling through the sample-then-pure structure of the real game; and PRG_Adv_zero_of_rHoare collapses the advantage to 0.

A bijection forces |Seed| = |Output|, so a bijection generator is not length-extending. This is the information-theoretic boundary of Rosulek §5: a genuinely length-extending PRG has an image that is a vanishing subset of the output space, so it can only be computationally secure. The corresponding reduction — the triple-from-double bound Adv(G₃) ≤ 2·Adv(G) — is proved computationally elsewhere (CatCrypt.Examples.TriplePRG).

Main definitions

• PRGScheme — a length-preserving/extending generator stretch : Seed → Output.
• PRG_Real / PRG_Ideal / PRG_Adv — the PRG distinguishing game and advantage.
• BijPRG — a seed→output bijection.
• BijPRG.toPRGScheme — the PRGScheme it induces (stretch s = bij s).

Main results

• PRG_Adv_zero_of_rHoare — a perfectly-indistinguishable PRG has advantage 0.
• bijPRG_coupling — the real and ideal PRG games couple with eqPost.
• bijPRG_perfect — a bijection PRG has perfect security: PRG_Adv B.toPRGScheme A = 0 for every adversary A.

References

• [Rosulek, The Joy of Cryptography, §5 (pseudorandom generators)]

PRG Scheme and Game

structure CatCrypt.Examples.PRG.PRGScheme : Type 1

A pseudorandom generator: a deterministic map stretch from a seed space to an output space.

Security asks that, for a uniform seed, stretch s is indistinguishable from a uniform element of Output.

• Seed : Type

  Seed (input) type

• Output : Type

  Output (stretched) type

• finSeed : Fintype self.Seed
• neSeed : Nonempty self.Seed
• finOutput : Fintype self.Output
• neOutput : Nonempty self.Output
• stretch : self.Seed → self.Output

  The deterministic stretch function

noncomputable def CatCrypt.Examples.PRG.PRG_Real (G : PRGScheme) : Core.SPComp G.Output

PRG real game: stretch a uniformly random seed.

Equations

• CatCrypt.Examples.PRG.PRG_Real G = do let s ← CatCrypt.Core.SPComp.sample G.Seed CatCrypt.Core.SPComp.pure (G.stretch s)

noncomputable def CatCrypt.Examples.PRG.PRG_Ideal (G : PRGScheme) : Core.SPComp G.Output

PRG ideal game: return a uniformly random output.

Equations

• CatCrypt.Examples.PRG.PRG_Ideal G = CatCrypt.Core.SPComp.sample G.Output

noncomputable def CatCrypt.Examples.PRG.PRG_Adv (G : PRGScheme) (A : G.Output → Core.SPComp Bool) : ENNReal

PRG advantage: distinguishing the stretched seed from a uniform output.

Equations

• CatCrypt.Examples.PRG.PRG_Adv G A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.PRG.PRG_Real G) (CatCrypt.Examples.PRG.PRG_Ideal G) A

theorem CatCrypt.Examples.PRG.PRG_Adv_zero_of_rHoare (G : PRGScheme) (h : Relational.rHoare Relational.eqPre (PRG_Real G) (PRG_Ideal G) Relational.eqPost) (A : G.Output → Core.SPComp Bool) : PRG_Adv G A = 0

If a PRG's real game is perfectly indistinguishable from the ideal game, the PRG advantage is 0 for every adversary.

Bijection PRG

structure CatCrypt.Examples.PRG.BijPRG : Type 1

A PRG given by a bijection bij : Seed ≃ Output.

For a uniform seed, bij maps the uniform seed distribution onto the uniform output distribution, which is the source of perfect security.

• Seed : Type

  Seed type

• Output : Type

  Output type

• finSeed : Fintype self.Seed
• neSeed : Nonempty self.Seed
• finOutput : Fintype self.Output
• neOutput : Nonempty self.Output
• bij : self.Seed ≃ self.Output

  A bijection from seeds to outputs

def CatCrypt.Examples.PRG.BijPRG.toPRGScheme (B : BijPRG) : PRGScheme

The PRGScheme induced by a bijection: stretch s = bij s.

Equations

• B.toPRGScheme = { Seed := B.Seed, Output := B.Output, finSeed := B.finSeed, neSeed := ⋯, finOutput := B.finOutput, neOutput := ⋯, stretch := fun (s : B.Seed) => B.bij s }

Perfect Security

theorem CatCrypt.Examples.PRG.bijPRG_coupling (B : BijPRG) : Relational.rHoare Relational.eqPre (PRG_Real B.toPRGScheme) (PRG_Ideal B.toPRGScheme) Relational.eqPost

Coupling: for a bijection PRG the real and ideal games are equidistributed.

Over a uniform seed s, the real game returns bij s while the ideal game returns a fresh uniform output r; liftR_uniform_bij B.bij couples them so that bij s = r, so the two games agree pointwise.

theorem CatCrypt.Examples.PRG.bijPRG_perfect (B : BijPRG) (A : B.toPRGScheme.Output → Core.SPComp Bool) : PRG_Adv B.toPRGScheme A = 0

A bijection PRG has perfect security: every adversary has PRG advantage exactly 0.

Example: the XOR PRG over Bool

G(s) = s ⊕ c for a fixed mask c is the bijection boolXorBij c; it is a (non-extending) bijection generator and inherits perfect security.

def CatCrypt.Examples.PRG.boolXorPRG (c : Bool) : BijPRG

The XOR generator over Bool as a bijection PRG: bij = boolXorBij c.

Equations

• CatCrypt.Examples.PRG.boolXorPRG c = { Seed := Bool, Output := Bool, finSeed := Bool.fintype, neSeed := ⋯, finOutput := Bool.fintype, neOutput := ⋯, bij := CatCrypt.Prob.XorBij.boolXorBij c }

theorem CatCrypt.Examples.PRG.boolXorPRG_perfect (c : Bool) (A : (boolXorPRG c).toPRGScheme.Output → Core.SPComp Bool) : PRG_Adv (boolXorPRG c).toPRGScheme A = 0

The XOR generator over Bool has perfect PRG security.

PRG security assumption

The bijection results above are perfect (ε = 0). A genuinely length-extending generator can only be computationally secure, so the reduction below takes the base generator's security as a hypothesis. PRGAssumption is the PRG analogue of CatCrypt.Crypto.PRFAssumption: it packages the standard "G is an ε-secure PRG" hypothesis that reductions consume.

structure CatCrypt.Examples.PRG.PRGAssumption (G : PRGScheme) : Type

The PRG security assumption: G is an ε-secure pseudorandom generator. The field bound witnesses that no adversary beats advantage ε at distinguishing PRG_Real G from PRG_Ideal G.

• ε : ENNReal

  The PRG advantage bound ε.

• bound (A : G.Output → Core.SPComp Bool) : PRG_Adv G A ≤ self.ε

  Every adversary has PRG advantage at most ε.

theorem CatCrypt.Examples.PRG.PRGAssumption.advantage_bound {G : PRGScheme} (H : PRGAssumption G) (A : G.Output → Core.SPComp Bool) : PRG_Adv G A ≤ H.ε

The packaged advantage bound of a PRG assumption.

def CatCrypt.Examples.PRG.PRGAssumption.of_perfect (G : PRGScheme) (h : ∀ (A : G.Output → Core.SPComp Bool), PRG_Adv G A = 0) : PRGAssumption G

A perfectly secure PRG (every adversary has advantage exactly 0) satisfies the PRG assumption with ε = 0.

Equations

• CatCrypt.Examples.PRG.PRGAssumption.of_perfect G h = { ε := 0, bound := ⋯ }

bind_vcgen witness for the ε = 0 case

For a bijection PRG the real and ideal games are the same SPComp distribution. We discharge this exact hop with the bind_vcgen run-to-completion tactic: through the supplied change-of-variables bijection B.bij it collapses sample s; return bij s to a fresh uniform sample. This is the perfect (ε = 0) base case that instantiates PRGAssumption.

theorem CatCrypt.Examples.PRG.bijPRG_game_eq (B : BijPRG) : PRG_Real B.toPRGScheme = PRG_Ideal B.toPRGScheme

The real and ideal PRG games for a bijection PRG are the same SPComp computation. Proved by bind_vcgen using B.bij: the change-of-variables through the bijection rewrites the stretched seed into a plain uniform sample.

theorem CatCrypt.Examples.PRG.bijPRG_adv_zero_via_vcgen (B : BijPRG) (A : B.toPRGScheme.Output → Core.SPComp Bool) : PRG_Adv B.toPRGScheme A = 0

A bijection PRG has PRG advantage 0, re-proved through the bind_vcgen game-equality bijPRG_game_eq (an alternative to the relational coupling of bijPRG_perfect).

noncomputable def CatCrypt.Examples.PRG.bijPRG_assumption (B : BijPRG) : PRGAssumption B.toPRGScheme

A bijection PRG satisfies the PRGAssumption with ε = 0, witnessed by the bind_vcgen proof bijPRG_adv_zero_via_vcgen.

Equations

• CatCrypt.Examples.PRG.bijPRG_assumption B = CatCrypt.Examples.PRG.PRGAssumption.of_perfect B.toPRGScheme ⋯

Triple-from-double PRG: the computational bound

Given a length-doubling base generator G : Seed → Seed × Seed, the length-tripling construction

`G₃(s) = let (a, b) := G(s); let (c, d) := G(a); (c, d, b)`

satisfies Adv_PRG(G₃) ≤ 2·ε under a PRG-security assumption on G (Rosulek, The Joy of Cryptography, §5.3). This mirrors the cascade-PRF upgrade (CatCrypt.Examples.PRF.cascade_prf_bound): a computational bound composed from two named per-hop assumptions via the advantage triangle inequality, keeping the perfect (ε = 0) corollary.

The reduction runs the decomposed hybrid (Rosulek §5.3), which uses independent seeds for the two G calls to break their correlation:

Step	Transition	Bound
0→1	inner G(s₁) (produces c,d) → random	ε (PRG assumption)
1→2	outer G(s₂).2 (produces b) → random	ε (PRG assumption)

The hop bounds are the cryptographic hypotheses; the theorem composes them into the total bound by the advantage triangle inequality.

structure CatCrypt.Examples.PRG.DoublePRG : Type 1

A length-doubling base generator stretch : Seed → Seed × Seed, the input to the triple construction.

• Seed : Type

  Seed type

• finSeed : Fintype self.Seed
• neSeed : Nonempty self.Seed
• stretch : self.Seed → self.Seed × self.Seed

  The length-doubling stretch function

def CatCrypt.Examples.PRG.DoublePRG.triple (G : DoublePRG) (s : G.Seed) : G.Seed × G.Seed × G.Seed

The length-tripling construction: apply G twice, rearrange outputs.

Equations

• G.triple s = match G.stretch s with | (a, b) => match G.stretch a with | (c, d) => (c, d, b)

def CatCrypt.Examples.PRG.DoublePRG.toInnerPRG (G : DoublePRG) : PRGScheme

The base doubling generator as a PRGScheme (Output = Seed × Seed), whose security is the inner-hop assumption.

Equations

• G.toInnerPRG = { Seed := G.Seed, Output := G.Seed × G.Seed, finSeed := G.finSeed, neSeed := ⋯, finOutput := instFintypeProd G.Seed G.Seed, neOutput := ⋯, stretch := G.stretch }

def CatCrypt.Examples.PRG.DoublePRG.toOuterPRG (G : DoublePRG) : PRGScheme

The projected doubling generator as a PRGScheme (Output = Seed, the second component), whose security is the outer-hop assumption.

Equations

• G.toOuterPRG = { Seed := G.Seed, Output := G.Seed, finSeed := G.finSeed, neSeed := ⋯, finOutput := G.finSeed, neOutput := ⋯, stretch := fun (s : G.Seed) => (G.stretch s).2 }

noncomputable def CatCrypt.Examples.PRG.DoublePRG.hyb (G : DoublePRG) (i : ℕ) : Core.SPComp (G.Seed × G.Seed × G.Seed)

Decomposed hybrid game (independent seeds per G call).

• i ≥ 2: everything uniform (ideal G₃);
• i = 1: inner G call replaced by random, outer G still real;
• i = 0: both G calls real but with independent seeds.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Examples.PRG.DoublePRG.hyb_2_ideal (G : DoublePRG) : G.hyb 2 = do let c ← Core.SPComp.sample G.Seed let d ← Core.SPComp.sample G.Seed let b ← Core.SPComp.sample G.Seed Core.SPComp.pure (c, d, b)

Hybrid 2 is the ideal G₃: three independent uniform seeds, independent of the base generator's stretch.

theorem CatCrypt.Examples.PRG.triple_prg_hybrid_bound {α : Type} (H : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (ε : ENNReal) (h01 : Crypto.AdvantageA (H 0) (H 1) A ≤ ε) (h12 : Crypto.AdvantageA (H 1) (H 2) A ≤ ε) : Crypto.AdvantageA (H 0) (H 2) A ≤ 2 * ε

Triple-from-double hybrid bound (the composition core).

For any 3-game hybrid sequence H realising the 2-hop ladder, if both hops are bounded by ε, then Adv(H₀, H₂) ≤ 2·ε. The composition is the advantage triangle inequality — the PRG analogue of cascade_prf_bound.

theorem CatCrypt.Examples.PRG.triple_prg_uniform_bound (G : DoublePRG) (ε : ENNReal) (A : G.Seed × G.Seed × G.Seed → Core.SPComp Bool) (h_inner : Crypto.AdvantageA (G.hyb 0) (G.hyb 1) A ≤ ε) (h_outer : Crypto.AdvantageA (G.hyb 1) (G.hyb 2) A ≤ ε) : Crypto.AdvantageA (G.hyb 0) (G.hyb 2) A ≤ 2 * ε

Triple PRG uniform bound: when both decomposed hybrid hops have advantage at most ε, the triple construction advantage is at most 2·ε.

This is the tight reduction Adv_PRG(G₃) ≤ 2·Adv_PRG(G), mirroring the dev CatCrypt.Examples.TriplePRG.triple_prg_uniform_bound.

theorem CatCrypt.Examples.PRG.triple_prg_bound_of_assumption (G : DoublePRG) (Hin : PRGAssumption G.toInnerPRG) (Hout : PRGAssumption G.toOuterPRG) (hε : Hout.ε ≤ Hin.ε) (A : G.Seed × G.Seed × G.Seed → Core.SPComp Bool) (Ain : G.toInnerPRG.Output → Core.SPComp Bool) (Aout : G.toOuterPRG.Output → Core.SPComp Bool) (h_inner : Crypto.AdvantageA (G.hyb 0) (G.hyb 1) A ≤ PRG_Adv G.toInnerPRG Ain) (h_outer : Crypto.AdvantageA (G.hyb 1) (G.hyb 2) A ≤ PRG_Adv G.toOuterPRG Aout) : Crypto.AdvantageA (G.hyb 0) (G.hyb 2) A ≤ 2 * Hin.ε

Triple PRG bound from a base-PRG security assumption.

If the inner and outer decomposed hops are bounded by the corresponding base-PRG advantages (h_inner, h_outer — the reduction's soundness, whose reduction adversaries Ain/Aout are exposed as hypotheses), and the base generator satisfies a PRGAssumption on each induced scheme (with Hout.ε ≤ Hin.ε), then the triple advantage is at most 2·Hin.ε.

theorem CatCrypt.Examples.PRG.triple_prg_perfect (G : DoublePRG) (A : G.Seed × G.Seed × G.Seed → Core.SPComp Bool) (h_inner : Crypto.AdvantageA (G.hyb 0) (G.hyb 1) A ≤ 0) (h_outer : Crypto.AdvantageA (G.hyb 1) (G.hyb 2) A ≤ 0) : Crypto.AdvantageA (G.hyb 0) (G.hyb 2) A = 0

Perfect triple corollary. When both hops are perfectly indistinguishable (ε = 0, e.g. a bijection base generator via bijPRG_assumption), the triple advantage is exactly 0.