feat(Crypto): define PRGs and their security definition

Cslib.lean

@@ -57,6 +57,9 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Primitives.PRG.Asymptotic
+public import Cslib.Crypto.Primitives.PRG.Basic
+public import Cslib.Crypto.Primitives.PRG.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption

Cslib/Crypto/Primitives/PRG/Asymptotic.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Crypto.Primitives.PRG.Basic
+public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
+public import Mathlib.Data.FinEnum
+
+/-!
+# Asymptotic pseudorandom generator security
+
+Security for families of generators means negligible advantage for each admissible
+adversary family, following [BonehShoup2023], Definition 3.1. Negligibility uses Mathlib's
+`Asymptotics.SuperpolynomialDecay`. Admissibility is a predicate on the whole adversary
+family, so a downstream computational model can express a uniform resource restriction.
+This model has a natural-number security parameter and no sampled public system parameters.
+Efficiency of generation and sampling is not asserted by these semantic definitions.
+
+If the range test is admissible and the seed space is eventually at most half the output
+space, security is impossible: the advantage is eventually at least one half. In particular,
+no family stretching bitstrings by at least one bit is secure against arbitrary adversaries.
+Mere strict cardinality expansion for arbitrary finite spaces would not give this constant
+gap, which is why the asymptotic theorem states the quantitative hypothesis explicitly.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG
+
+open Filter
+open scoped Topology
+
+/-- A security-parameter-indexed collection of deterministic generators. -/
+abbrev Family (Seed Output : ℕ → Type*) := ∀ n, Generator (Seed n) (Output n)
+
+namespace Family
+
+variable {Seed Output : ℕ → Type*}
+variable [∀ n, Fintype (Seed n)] [∀ n, Nonempty (Seed n)]
+variable [∀ n, Fintype (Output n)] [∀ n, Nonempty (Output n)]
+
+/-- Every admissible adversary family has negligible distinguishing advantage.
+The predicate can encode computational restrictions; `fun _ => True` permits all families. -/
+def Secure (G : Family Seed Output)
+    (Admissible : (∀ n, Adversary (Output n)) → Prop) : Prop :=
+  ∀ adversary, Admissible adversary →
+    Asymptotics.SuperpolynomialDecay atTop (fun n : ℕ => (n : ℝ))
+      (fun n => (G n).advantage (adversary n))
+
+/-- Restricting the admissible adversary families preserves asymptotic security. -/
+theorem Secure.of_admissible {G : Family Seed Output}
+    {Admissible Restricted : (∀ n, Adversary (Output n)) → Prop}
+    (h : G.Secure Admissible) (hsub : ∀ adversary, Restricted adversary → Admissible adversary) :
+    G.Secure Restricted := fun adversary ha => h adversary (hsub adversary ha)
+
+/-- A constant positive lower bound on the range test's advantage rules out security. -/
+theorem not_secure_of_rangeAdversary (G : Family Seed Output)
+    {Admissible : (∀ n, Adversary (Output n)) → Prop}
+    (ha : Admissible (fun n => (G n).rangeAdversary))
+    {δ : ℝ} (hδ : 0 < δ)
+    (hgap : ∀ᶠ n in atTop,
+      δ ≤ 1 - Fintype.card (Seed n) / (Fintype.card (Output n) : ℝ)) :
+    ¬ G.Secure Admissible := by
+  intro h
+  have hlim : Tendsto (fun n => (G n).advantage (G n).rangeAdversary) atTop (𝓝 0) := by
+    simpa using h _ ha 0
+  have hle : δ ≤ 0 := ge_of_tendsto hlim (hgap.mono fun n hn =>
+    hn.trans (G n).one_sub_card_div_le_advantage_rangeAdversary)
+  exact hδ.not_ge hle
+
+/-- If the output space is eventually at least twice as large as the seed space,
+then security against arbitrary adversaries is impossible. -/
+theorem not_secure_of_two_mul_card_le (G : Family Seed Output)
+    (hsize : ∀ᶠ n in atTop, 2 * Fintype.card (Seed n) ≤ Fintype.card (Output n)) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_rangeAdversary trivial (δ := 1 / 2) (by norm_num)
+  filter_upwards [hsize] with n hn
+  have hpos : (0 : ℝ) < Fintype.card (Output n) := by exact_mod_cast Fintype.card_pos
+  have hcard : 2 * (Fintype.card (Seed n) : ℝ) ≤ Fintype.card (Output n) := by
+    exact_mod_cast hn
+  have hratio : Fintype.card (Seed n) / (Fintype.card (Output n) : ℝ) ≤ 1 / 2 :=
+    (div_le_iff₀ hpos).mpr (by linarith)
+  linarith
+
+/-- No bitstring generator family stretching by at least one bit is secure against
+arbitrary adversaries, even when stretching is only required eventually. -/
+theorem not_secure_of_bitstring_stretch {seedLength outputLength : ℕ → ℕ}
+    (G : Family (fun n => Fin (seedLength n) → Bool) (fun n => Fin (outputLength n) → Bool))
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_two_mul_card_le
+  filter_upwards [hstretch] with n hn
+  simp only [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin]
+  calc
+    2 * 2 ^ seedLength n = 2 ^ (seedLength n + 1) := by rw [pow_succ, mul_comm]
+    _ ≤ 2 ^ outputLength n := Nat.pow_le_pow_right (by decide) hn
+
+/-- No family that eventually stretches bitstrings is secure against arbitrary adversaries. -/
+theorem not_exists_secure_bitstring_stretch {seedLength outputLength : ℕ → ℕ}
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ ∃ G : Family (fun n => Fin (seedLength n) → Bool)
+      (fun n => Fin (outputLength n) → Bool), G.Secure (fun _ => True) := by
+  rintro ⟨G, hG⟩
+  exact G.not_secure_of_bitstring_stretch hstretch hG
+
+/-- The impossibility of stretching against arbitrary adversaries, using `BitVec`. -/
+theorem not_secure_of_bitVec_stretch {seedLength outputLength : ℕ → ℕ}
+    (G : Family (fun n => BitVec (seedLength n)) (fun n => BitVec (outputLength n)))
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_two_mul_card_le
+  filter_upwards [hstretch] with n hn
+  simp only [← FinEnum.card_eq_fintypeCard, FinEnum.card_bitVec]
+  calc
+    2 * 2 ^ seedLength n = 2 ^ (seedLength n + 1) := by rw [pow_succ, mul_comm]
+    _ ≤ 2 ^ outputLength n := Nat.pow_le_pow_right (by decide) hn
+
+/-- There is no secure expanding `BitVec` generator family against arbitrary adversaries. -/
+theorem not_exists_secure_bitVec_stretch {seedLength outputLength : ℕ → ℕ}
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ ∃ G : Family (fun n => BitVec (seedLength n)) (fun n => BitVec (outputLength n)),
+      G.Secure (fun _ => True) := by
+  rintro ⟨G, hG⟩
+  exact G.not_secure_of_bitVec_stretch hstretch hG
+
+end Family
+end Cslib.Crypto.PRG

Cslib/Crypto/Primitives/PRG/Basic.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Crypto.Primitives.PRG.Defs
+
+/-!
+# Pseudorandom generators against arbitrary adversaries
+
+The range-membership test accepts every generated output, whereas it accepts a uniform
+output with probability `|range G| / |Output|`. Its advantage is therefore at least
+`1 - |Seed| / |Output|`. This proves that an expanding generator cannot have zero
+advantage against arbitrary adversaries, and gives a quantitative obstruction for
+every smaller error bound. No injectivity assumption on the generator is needed.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG.Generator
+
+open scoped NNReal
+
+variable {Seed Output : Type*}
+
+/-- An unbounded adversary tests whether its input is in the generator's range.
+It is not assumed to be admissible for a computationally restricted class. -/
+noncomputable def rangeAdversary (G : Generator Seed Output) : Adversary Output := by
+  classical
+  exact fun output => PMF.pure (decide (output ∈ Set.range G))
+
+variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+
+/-- Advantage is nonnegative. -/
+theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Output) :
+    0 ≤ G.advantage adversary := abs_nonneg _
+
+/-- Advantage is at most one, with the normalization of Attack Game 3.1. -/
+theorem advantage_le_one (G : Generator Seed Output) (adversary : Adversary Output) :
+    G.advantage adversary ≤ 1 := by
+  have hreal := ENNReal.toReal_mono ENNReal.one_ne_top
+    (PMF.coe_le_one (G.realExperiment adversary) true)
+  have hideal := ENNReal.toReal_mono ENNReal.one_ne_top
+    (PMF.coe_le_one (idealExperiment adversary) true)
+  simp only [ENNReal.toReal_one] at hreal hideal
+  apply abs_sub_le_iff.mpr
+  constructor
+  · linarith [@ENNReal.toReal_nonneg (idealExperiment adversary true)]
+  · linarith [@ENNReal.toReal_nonneg (G.realExperiment adversary true)]
+
+/-- Error one imposes no restriction on a generator. -/
+theorem secure_one (G : Generator Seed Output) (Admissible : Adversary Output → Prop) :
+    G.Secure Admissible 1 := fun adversary _ => G.advantage_le_one adversary
+
+/-- A test whose output distribution is independent of its input has zero advantage. -/
+@[simp]
+theorem advantage_const (G : Generator Seed Output) (p : PMF Bool) :
+    G.advantage (fun _ => p) = 0 := by
+  simp [advantage, realExperiment, idealExperiment, PMF.bind_const]
+
+/-- A generator with exactly uniform output is secure with zero error against any tests. -/
+theorem secure_zero_of_outputDist_eq (G : Generator Seed Output)
+    (hG : G.outputDist = PMF.uniformOfFintype Output)
+    (Admissible : Adversary Output → Prop) : G.Secure Admissible 0 := by
+  intro adversary _
+  simp [advantage, realExperiment, idealExperiment, hG]
+
+/-- Zero-error security against arbitrary tests is equivalent to exactly uniform output. -/
+theorem secure_zero_iff_outputDist_eq_uniform (G : Generator Seed Output) :
+    G.Secure (fun _ => True) 0 ↔ G.outputDist = PMF.uniformOfFintype Output := by
+  classical
+  refine ⟨fun h => ?_, fun h => G.secure_zero_of_outputDist_eq h _⟩
+  ext output
+  apply (ENNReal.toReal_eq_toReal_iff' (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)).mp
+  simpa [advantage, realExperiment, idealExperiment, PMF.bind_apply, PMF.pure_apply,
+    sub_eq_zero] using h (fun x => PMF.pure (decide (x = output))) trivial
+
+/-- Enlarging the allowed advantage preserves security. -/
+theorem Secure.mono {G : Generator Seed Output} {Admissible : Adversary Output → Prop} :
+    Monotone (G.Secure Admissible) :=
+  fun _ _ hεδ h adversary ha => (h adversary ha).trans (by exact_mod_cast hεδ)
+
+/-- Security against a larger class of adversaries implies security against a smaller class. -/
+theorem Secure.of_admissible {G : Generator Seed Output}
+    {Admissible Restricted : Adversary Output → Prop} {ε : ℝ≥0}
+    (h : G.Secure Admissible ε) (hsub : ∀ adversary, Restricted adversary → Admissible adversary) :
+    G.Secure Restricted ε := fun adversary ha => h adversary (hsub adversary ha)
+
+omit [Fintype Output] [Nonempty Output] in
+/-- The range test always accepts a generated output. -/
+@[simp]
+theorem realExperiment_rangeAdversary (G : Generator Seed Output) :
+    G.realExperiment G.rangeAdversary = PMF.pure true := by
+  simp [realExperiment, outputDist, PMF.bind_map, rangeAdversary, Function.comp_def,
+    PMF.bind_const]
+
+omit [Fintype Seed] [Nonempty Seed] in
+/-- The range test's acceptance probability under uniform sampling is the fraction
+of outputs in the range. -/
+theorem idealExperiment_rangeAdversary (G : Generator Seed Output) :
+    (idealExperiment G.rangeAdversary true).toReal =
+      Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
+  classical
+  simp only [idealExperiment, rangeAdversary, PMF.bind_apply, PMF.pure_apply,
+    PMF.uniformOfFintype_apply, tsum_fintype]
+  simp only [mul_ite, mul_one, mul_zero, eq_comm (a := true), decide_eq_true_eq]
+  rw [← Finset.sum_filter]
+  simp [Nat.card_eq_fintype_card, Fintype.card_subtype, div_eq_mul_inv]
+
+/-- The exact advantage of the range-membership adversary. -/
+theorem advantage_rangeAdversary (G : Generator Seed Output) :
+    G.advantage G.rangeAdversary =
+      1 - Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
+  have hprob : (idealExperiment G.rangeAdversary true).toReal ≤ 1 :=
+    (ENNReal.toReal_le_toReal (PMF.apply_ne_top _ _) ENNReal.one_ne_top).mpr
+      (PMF.coe_le_one _ _)
+  rw [advantage, realExperiment_rangeAdversary]
+  simp only [PMF.pure_apply, ↓reduceIte, ENNReal.toReal_one]
+  rw [abs_of_nonneg (sub_nonneg.mpr hprob), idealExperiment_rangeAdversary]
+
+/-- Every generator has an unbounded distinguisher with advantage at least
+`1 - |Seed| / |Output|`. Collisions can only improve this attack. -/
+theorem one_sub_card_div_le_advantage_rangeAdversary (G : Generator Seed Output) :
+    1 - Fintype.card Seed / (Fintype.card Output : ℝ) ≤
+      G.advantage G.rangeAdversary := by
+  classical
+  rw [advantage_rangeAdversary]
+  have hcard : Nat.card (Set.range G) ≤ Fintype.card Seed := by
+    simpa using Fintype.card_range_le G
+  gcongr
+
+/-- Security is impossible below the range-test bound whenever that test is admissible. -/
+theorem not_secure_of_rangeAdversary (G : Generator Seed Output)
+    {Admissible : Adversary Output → Prop} {ε : ℝ≥0}
+    (ha : Admissible G.rangeAdversary)
+    (hε : (ε : ℝ) < 1 - Fintype.card Seed / (Fintype.card Output : ℝ)) :
+    ¬ G.Secure Admissible ε := by
+  intro h
+  exact (hε.trans_le G.one_sub_card_div_le_advantage_rangeAdversary).not_ge (h _ ha)
+
+/-- An expanding generator cannot be perfectly secure against arbitrary adversaries. -/
+theorem not_secure_zero_of_isExpanding (G : Generator Seed Output) (hG : G.IsExpanding) :
+    ¬ G.Secure (fun _ => True) 0 := by
+  apply G.not_secure_of_rangeAdversary trivial
+  have hpos : (0 : ℝ) < Fintype.card Output := by exact_mod_cast Fintype.card_pos
+  have hlt : (Fintype.card Seed : ℝ) < Fintype.card Output := by exact_mod_cast hG
+  simpa using sub_pos.mpr ((div_lt_one hpos).mpr hlt)
+
+/-- There is no expanding, perfectly secure generator against arbitrary adversaries. -/
+theorem not_exists_isExpanding_secure_zero :
+    ¬ ∃ G : Generator Seed Output, G.IsExpanding ∧ G.Secure (fun _ => True) 0 := by
+  rintro ⟨G, hG, hsecure⟩
+  exact G.not_secure_zero_of_isExpanding hG hsecure
+
+end Cslib.Crypto.PRG.Generator

Cslib/Crypto/Primitives/PRG/Defs.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Probability.Distributions.Uniform
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+/-!
+# Pseudorandom generators: games and concrete security
+
+Attack Game 3.1 of [BonehShoup2023] compares a deterministic generator applied to a
+uniform seed with a uniform output. Adversaries are randomized Boolean tests. Security
+is relative to a caller-supplied predicate `Admissible`, with an explicit advantage bound.
+No computational model or efficiency assumption is built into the generator or the tests.
+
+`Generator.IsExpanding` records the cardinality condition separately from security.
+In particular, a generator need not expand, and an expanding generator need not be secure.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Section 3.1.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG
+
+open scoped NNReal
+
+/-- A deterministic generator with seed space `Seed` and output space `Output`.
+Efficiency, expansion, and security are separate properties. -/
+@[ext]
+structure Generator (Seed Output : Type*) where
+  /-- Generate an output from a seed. -/
+  toFun : Seed → Output
+
+/-- A randomized statistical test on the output space. -/
+abbrev Adversary (Output : Type*) := Output → PMF Bool
+
+namespace Generator
+
+variable {Seed Output : Type*}
+
+instance : FunLike (Generator Seed Output) Seed Output where
+  coe G := G.toFun
+  coe_injective _ _ h := Generator.ext h
+
+@[simp]
+theorem coe_mk (f : Seed → Output) : ⇑(Generator.mk f) = f := rfl
+
+/-- A generator expands when its output space is strictly larger than its seed space. -/
+def IsExpanding [Fintype Seed] [Fintype Output] (_G : Generator Seed Output) : Prop :=
+  Fintype.card Seed < Fintype.card Output
+
+variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+
+/-- The distribution obtained by applying the generator to a uniform seed. -/
+noncomputable def outputDist (G : Generator Seed Output) : PMF Output :=
+  (PMF.uniformOfFintype Seed).map G
+
+/-- Experiment 0 of Attack Game 3.1: give the adversary a generated output. -/
+noncomputable def realExperiment (G : Generator Seed Output)
+    (adversary : Adversary Output) : PMF Bool :=
+  G.outputDist.bind adversary
+
+/-- Experiment 1 of Attack Game 3.1: give the adversary a uniform output. -/
+noncomputable def idealExperiment (adversary : Adversary Output) : PMF Bool :=
+  (PMF.uniformOfFintype Output).bind adversary
+
+/-- The absolute difference of the probabilities of outputting `true` in the two
+experiments, as in Attack Game 3.1 of [BonehShoup2023]. -/
+noncomputable def advantage (G : Generator Seed Output) (adversary : Adversary Output) : ℝ :=
+  |(G.realExperiment adversary true).toReal - (idealExperiment adversary true).toReal|
+
+/-- Concrete security against admissible adversaries. The predicate is supplied by the
+caller, for example to restrict tests to a chosen computational resource bound.
+Taking `Admissible := fun _ => True` allows arbitrary adversaries. -/
+def Secure (G : Generator Seed Output) (Admissible : Adversary Output → Prop)
+    (ε : ℝ≥0) : Prop :=
+  ∀ adversary, Admissible adversary → G.advantage adversary ≤ ε
+
+end Generator
+end Cslib.Crypto.PRG