From c7bc0684ff92263671bd7e6d3aaccabec2d305ca Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 17:32:58 +0000 Subject: [PATCH 1/2] feat(crypto): Carter-Wegman PRF-masked one-time pad bridge (#736) Complete Criterion 4 of #736 in Complexity/Crypto/Protocols/MAC/CarterWegman.lean: - Add maskedOneTimeGame_toReal_le_add_advantage and maskedOneTimeStrongGame_toReal_le_add_advantage phrasing the Boneh-Shoup Theorem 7.4 hybrid bound in terms of Game.advantage. - Define OneTimeForger.ofProbComp and probPadTest (with eval_probPadTest) for ProbComp hash-key samplers and one-time forgers. - Define prfPadDist, prfOneTimeGame, prfOneTimeStrongGame (with prfOneTimeStrongGame_eq_prfOneTimeGame), and the single-query OracleDistinguisher adapter prfPadDistinguisher. - Prove eval_prfRealGame_prfPadDistinguisher, map_eval_uniformOfFintype_fun, and eval_prfIdealGame_prfPadDistinguisher. - Prove prfOneTimeGame_le_of_distinguisher, prfOneTimeGame_le, prfOneTimeStrongGame_le, prfOneTimeGame_ofProbComp_le, prfOneTimeStrongGame_ofProbComp_le, and prfOneTimeGame_linearHash_le. - Add concrete nonvacuous checks and #print axioms guards in ComplexityTests/Crypto/CarterWegman.lean and update ROADMAP.md. Closes #736 Refs #640 --- .../Crypto/Protocols/MAC/CarterWegman.lean | 287 +++++++++++++++++- ComplexityTests/Crypto/CarterWegman.lean | 99 +++++- ROADMAP.md | 19 +- 3 files changed, 386 insertions(+), 19 deletions(-) diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index 6e815a9fc5..2aa28efecd 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Crypto.Computational.PseudorandomFunction public import Complexity.Languages.Probabilistic.Simulation public import Complexity.Probability.BitString.LinearHash public import Complexity.Probability.BitString.SubsetSum @@ -62,12 +63,17 @@ This module formalizes: Unissued counter indices (`pads[idx]? = none`) are rejected (`false`), so zero-query success in the issued-counter games is `0` (whereas the standalone `zeroQueryGame` has success `1 / |Y|`); a fresh-counter experiment that accepts unissued nonces against fresh pads is separate scope. -5. **Arbitrary-pad hybrid decomposition (`maskedOneTimeGame`, `padDistinguisher`, - `maskedOneTimeGame_toReal_le`)**: replacing the uniform pad `r ← PMF.uniformOfFintype Y` with - any pad distribution `padDist : PMF Y` bounds the real forgery probability by `ε.toReal` plus - the distinguishing advantage of `padDistinguisher` between `padDist` and - `PMF.uniformOfFintype Y` ([BonehShoup2023], Theorem 7.4). Connecting `padDist` to a computational - PRF security game is left as follow-up work. +5. **Arbitrary-pad and PRF-masked hybrid decomposition (`maskedOneTimeGame`, `padDistinguisher`, + `maskedOneTimeGame_toReal_le`, `maskedOneTimeGame_toReal_le_add_advantage`, `prfPadDist`, + `prfOneTimeGame`, `prfOneTimeStrongGame`, `prfPadDistinguisher`, `prfOneTimeGame_le`, + `prfOneTimeStrongGame_le`, `prfOneTimeGame_ofProbComp_le`)**: replacing the uniform pad + `r ← PMF.uniformOfFintype Y` with any pad distribution `padDist : PMF Y` bounds the real forgery + probability by `ε.toReal` plus the distinguishing advantage of `padDistinguisher` between + `padDist` and `PMF.uniformOfFintype Y` ([BonehShoup2023], Theorem 7.4). When `Y = BitString n` + and the pad is generated by evaluating a PRF family `family` at `List.replicate n false` under a + uniform `n`-bit key (`prfPadDist family n`), the single-query `OracleDistinguisher` adapter + `prfPadDistinguisher` connects the real and ideal pad experiments directly to `prfRealGame` and + `prfIdealGame`, bounding one-time forgery probability by `ε.toReal` plus the PRF advantage. 6. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash`, bound `2⁻ᵐ`), subset-sum hashing (`BitString.SubsetSum.hash`, bound `1 / |G|`), and pairwise independent @@ -88,8 +94,14 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.counterStrongGame`: adaptive multi-query issued-counter Carter–Wegman experiments. * `Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame`, - `Cslib.Crypto.Protocols.CarterWegman.padDistinguisher`: arbitrary-pad one-time Carter–Wegman - experiment and its induced pad distinguisher. + `Cslib.Crypto.Protocols.CarterWegman.padDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.probPadTest`: arbitrary-pad one-time Carter–Wegman + experiment and its induced `PMF` and `ProbComp` pad distinguishers. +* `Cslib.Crypto.Protocols.CarterWegman.prfPadDist`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame`, + `Cslib.Crypto.Protocols.CarterWegman.prfPadDistinguisher`: PRF-masked one-time Carter–Wegman + experiments and the single-query `OracleDistinguisher` adapter. ## Main results @@ -103,11 +115,20 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.counterGame_le`, `Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_le`: multi-query issued-counter Carter–Wegman security (`≤ ε`). -* `Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le`: arbitrary-pad hybrid bound. +* `Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le`, + `Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le_add_advantage`: arbitrary-pad + hybrid bounds. +* `Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfPadDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le`: PRF-masked one-time + Carter–Wegman security (Boneh–Shoup Theorem 7.4). * `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le`, `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_linearHash_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_linearHash_le`, + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_linearHash_le`, `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_subsetSum_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_subsetSum_le`, `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_of_isPairwiseIndependentHash_le`, @@ -673,8 +694,231 @@ theorem maskedOneTimeGame_toReal_le [Fintype Y] [Nonempty Y] {seed : PMF K} {has linarith [le_abs_self (((padDist.bind (padDistinguisher seed hash forger)) true).toReal - (oneTimeGame seed hash forger true).toReal)] +/-- `Game.advantage` form of `maskedOneTimeGame_toReal_le` ([BonehShoup2023], Section 7.4, +Theorem 7.4): the real-valued forgery probability under `padDist` is bounded by `ε.toReal` plus +`Game.advantage` between `padDist.bind (padDistinguisher seed hash forger)` and +`(PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)`. -/ +theorem maskedOneTimeGame_toReal_le_add_advantage [Fintype Y] [Nonempty Y] {seed : PMF K} + {hash : K → M → Y} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) + (padDist : PMF Y) (forger : OneTimeForger M Y) : + (maskedOneTimeGame seed padDist hash forger true).toReal ≤ + ε.toReal + + (Game.advantage (padDist.bind (padDistinguisher seed hash forger)) + ((PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)) : ℝ) := by + rw [Game.coe_advantage, Game.coe_succProbability, Game.coe_succProbability] + exact maskedOneTimeGame_toReal_le hh hε padDist forger + +/-- Strong-unforgeability version of `maskedOneTimeGame_toReal_le_add_advantage`. -/ +theorem maskedOneTimeStrongGame_toReal_le_add_advantage [Fintype Y] [Nonempty Y] {seed : PMF K} + {hash : K → M → Y} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) + (padDist : PMF Y) (forger : OneTimeForger M Y) : + (maskedOneTimeStrongGame seed padDist hash forger true).toReal ≤ + ε.toReal + + (Game.advantage (padDist.bind (padDistinguisher seed hash forger)) + ((PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)) : ℝ) := by + rw [maskedOneTimeStrongGame_eq_maskedOneTimeGame] + exact maskedOneTimeGame_toReal_le_add_advantage hh hε padDist forger + +/-- Construct a `OneTimeForger` from `ProbComp` query and forgery programs. -/ +noncomputable def OneTimeForger.ofProbComp (query : ProbComp M) + (forge : M → Y → ProbComp (M × Y)) : OneTimeForger M Y where + query := ProbComp.eval query + forge m t := ProbComp.eval (forge m t) + +/-- Executable `ProbComp` simulation of the one-time Carter–Wegman experiment with a supplied pad +`r : Y`, given `ProbComp` samplers for the hash key `seed`, signing query `query`, and forgery +attempt `forge`. -/ +def probPadTest (seed : ProbComp K) (hash : K → M → Y) (query : ProbComp M) + (forge : M → Y → ProbComp (M × Y)) (r : Y) : ProbComp Bool := do + let k ← seed + let m ← query + let p ← forge m (sign hash k r m) + return (decide (p.1 ≠ m) && verify hash k r p.1 p.2) + +@[simp] +theorem eval_probPadTest (seed : ProbComp K) (hash : K → M → Y) (query : ProbComp M) + (forge : M → Y → ProbComp (M × Y)) (r : Y) : + ProbComp.eval (probPadTest seed hash query forge r) = + padDistinguisher (ProbComp.eval seed) hash (OneTimeForger.ofProbComp query forge) r := by + simp [probPadTest, padDistinguisher, OneTimeForger.ofProbComp, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.map, Function.comp_def] + end MaskedPad +/-! ### PRF-masked one-time Carter–Wegman MAC (Boneh–Shoup Theorem 7.4) -/ + +section PRFPad + +variable {K M : Type} [DecidableEq M] + +/-- The one-time pad distribution on `BitString n` obtained by sampling a uniform `n`-bit PRF key +`key ← BitString.uniformList n` and evaluating `family key (List.replicate n false)`. -/ +noncomputable def prfPadDist (family : List Bool → List Bool → List Bool) (n : ℕ) : + PMF (BitString n) := + (BitString.uniformList n).map fun key => + BitString.ofList n (family key (List.replicate n false)) + +/-- The PRF-masked one-time Carter–Wegman EUF-CMA experiment ([BonehShoup2023], Section 7.4, +Theorem 7.4): the pad `r : BitString n` is generated by evaluating `family` on a uniform `n`-bit +PRF key at nonce `List.replicate n false`. -/ +noncomputable def prfOneTimeGame (seed : PMF K) (family : List Bool → List Bool → List Bool) + (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) : PMF Bool := + maskedOneTimeGame seed (prfPadDist family n) hash forger + +/-- The PRF-masked one-time Carter–Wegman SUF-CMA experiment. -/ +noncomputable def prfOneTimeStrongGame (seed : PMF K) + (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) + (forger : OneTimeForger M (BitString n)) : PMF Bool := + maskedOneTimeStrongGame seed (prfPadDist family n) hash forger + +theorem prfOneTimeStrongGame_eq_prfOneTimeGame (seed : PMF K) + (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) + (forger : OneTimeForger M (BitString n)) : + prfOneTimeStrongGame seed family n hash forger = + prfOneTimeGame seed family n hash forger := + maskedOneTimeStrongGame_eq_maskedOneTimeGame seed (prfPadDist family n) hash forger + +/-- Single-query PRF `OracleDistinguisher` induced by a family of `ProbComp` pad tests +`test : (n : ℕ) → BitString n → ProbComp Bool`: at security parameter `n`, query the oracle once at +the fixed nonce `List.replicate n false` and run `test n` on the `n`-bit view of the reply. -/ +def prfPadDistinguisher (test : (n : ℕ) → BitString n → ProbComp Bool) : + OracleDistinguisher := fun n _ => do + let reply ← ProbOracleComp.query ((), List.replicate n false) + ProbOracleComp.sample (test n (BitString.ofList n reply)) + +/-- In `prfRealGame`, `prfPadDistinguisher test` evaluates `test n` on a pad drawn from +`prfPadDist family n`. -/ +theorem eval_prfRealGame_prfPadDistinguisher (family : List Bool → List Bool → List Bool) + (test : (n : ℕ) → BitString n → ProbComp Bool) (n : ℕ) : + ProbComp.eval (prfRealGame family (prfPadDistinguisher test) n) = + (prfPadDist family n).bind (fun r => ProbComp.eval (test n r)) := by + simp only [prfRealGame, prfPadDistinguisher, prfPadDist, ProbComp.eval_bind, + BitString.eval_sampleList, PMF.bind_map, Function.comp_def] + congr 1 + funext key + simp [prfOracle, show ProbComp.unifFin = OracleComp.query from rfl] + +/-- Evaluating a uniformly random function `table : BitString n → BitString n` at any single point +`x : BitString n` produces the uniform distribution on `BitString n`. -/ +theorem map_eval_uniformOfFintype_fun (n : ℕ) (x : BitString n) : + (PMF.uniformOfFintype (BitString n → BitString n)).map (fun table => table x) = + PMF.uniformOfFintype (BitString n) := by + rw [← PMF.pi_uniformOfFintype, PMF.pi_map_eval] + +/-- In `prfIdealGame`, `prfPadDistinguisher test` evaluates `test n` on a uniform pad +`r ← PMF.uniformOfFintype (BitString n)`. -/ +theorem eval_prfIdealGame_prfPadDistinguisher (test : (n : ℕ) → BitString n → ProbComp Bool) + (n : ℕ) : + ProbComp.eval (prfIdealGame (prfPadDistinguisher test) n) = + (PMF.uniformOfFintype (BitString n)).bind (fun r => ProbComp.eval (test n r)) := by + conv_rhs => + rw [← map_eval_uniformOfFintype_fun n (BitString.ofList n (List.replicate n false)), + PMF.bind_map] + simp only [prfIdealGame, prfPadDistinguisher, ProbComp.eval_bind, ProbComp.eval_uniform, + Function.comp_def] + congr 1 + funext table + simp [randomFunctionOracle, show ProbComp.unifFin = OracleComp.query from rfl] + +/-- **PRF-masked Carter–Wegman bound for an explicit `OracleDistinguisher`** +([BonehShoup2023], Section 7.4, Theorem 7.4): if `D` simulates `padDistinguisher seed hash forger` +in both `prfRealGame` and `prfIdealGame`, then the real-valued one-time forgery probability is at +most `ε.toReal` plus the PRF distinguishing advantage of `D`. -/ +theorem prfOneTimeGame_le_of_distinguisher {n : ℕ} {seed : PMF K} + {hash : K → M → BitString n} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) + (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) + (D : OracleDistinguisher) + (hreal : ProbComp.eval (prfRealGame family D n) = + (prfPadDist family n).bind (padDistinguisher seed hash forger)) + (hideal : ProbComp.eval (prfIdealGame D n) = + (PMF.uniformOfFintype (BitString n)).bind (padDistinguisher seed hash forger)) : + (prfOneTimeGame seed family n hash forger true).toReal ≤ + ε.toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family D n)) + (ProbComp.eval (prfIdealGame D n)) : ℝ) := by + rw [hreal, hideal] + exact maskedOneTimeGame_toReal_le_add_advantage hh hε (prfPadDist family n) forger + +/-- **PRF-masked one-time Carter–Wegman EUF-CMA security** ([BonehShoup2023], Section 7.4, +Theorem 7.4): replacing the uniform pad `r ← PMF.uniformOfFintype (BitString n)` with the PRF pad +`prfPadDist family n` bounds the one-time forgery probability by `ε.toReal` plus the PRF +distinguishing advantage of `prfPadDistinguisher test`. -/ +theorem prfOneTimeGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) + (family : List Bool → List Bool → List Bool) + (forger : OneTimeForger M (BitString n)) + (test : (n : ℕ) → BitString n → ProbComp Bool) + (htest : ∀ r, padDistinguisher seed hash forger r = ProbComp.eval (test n r)) : + (prfOneTimeGame seed family n hash forger true).toReal ≤ + ε.toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family (prfPadDistinguisher test) n)) + (ProbComp.eval (prfIdealGame (prfPadDistinguisher test) n)) : ℝ) := by + refine prfOneTimeGame_le_of_distinguisher hh hε family forger (prfPadDistinguisher test) ?_ ?_ + · rw [eval_prfRealGame_prfPadDistinguisher] + congr 1; funext r; exact (htest r).symm + · rw [eval_prfIdealGame_prfPadDistinguisher] + congr 1; funext r; exact (htest r).symm + +/-- **PRF-masked one-time Carter–Wegman SUF-CMA security** ([BonehShoup2023], Section 7.4, +Theorem 7.4). -/ +theorem prfOneTimeStrongGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) + (family : List Bool → List Bool → List Bool) + (forger : OneTimeForger M (BitString n)) + (test : (n : ℕ) → BitString n → ProbComp Bool) + (htest : ∀ r, padDistinguisher seed hash forger r = ProbComp.eval (test n r)) : + (prfOneTimeStrongGame seed family n hash forger true).toReal ≤ + ε.toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family (prfPadDistinguisher test) n)) + (ProbComp.eval (prfIdealGame (prfPadDistinguisher test) n)) : ℝ) := by + rw [prfOneTimeStrongGame_eq_prfOneTimeGame] + exact prfOneTimeGame_le hh hε family forger test htest + +/-- **PRF-masked one-time Carter–Wegman bound for `ProbComp` samplers and forgers**: +any `ProbComp` hash-key sampler `seed`, query program `query`, and forgery program `forge` +automatically induce the single-query PRF distinguisher via `probPadTest`. -/ +theorem prfOneTimeGame_ofProbComp_le {n : ℕ} {seed : ProbComp K} + {hash : K → M → BitString n} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval seed) hash ε) (hε : ε ≠ ⊤) + (family : List Bool → List Bool → List Bool) + (query : ProbComp M) (forge : M → BitString n → ProbComp (M × BitString n)) : + (prfOneTimeGame (ProbComp.eval seed) family n hash + (OneTimeForger.ofProbComp query forge) true).toReal ≤ + ε.toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family + (prfPadDistinguisher fun _ r => + probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n)) + (ProbComp.eval (prfIdealGame + (prfPadDistinguisher fun _ r => + probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n)) : ℝ) := by + refine prfOneTimeGame_le hh hε family (OneTimeForger.ofProbComp query forge) _ fun r => ?_ + simp + +/-- Strong-unforgeability version of `prfOneTimeGame_ofProbComp_le`. -/ +theorem prfOneTimeStrongGame_ofProbComp_le {n : ℕ} {seed : ProbComp K} + {hash : K → M → BitString n} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval seed) hash ε) (hε : ε ≠ ⊤) + (family : List Bool → List Bool → List Bool) + (query : ProbComp M) (forge : M → BitString n → ProbComp (M × BitString n)) : + (prfOneTimeStrongGame (ProbComp.eval seed) family n hash + (OneTimeForger.ofProbComp query forge) true).toReal ≤ + ε.toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family + (prfPadDistinguisher fun _ r => + probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n)) + (ProbComp.eval (prfIdealGame + (prfPadDistinguisher fun _ r => + probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n)) : ℝ) := by + rw [prfOneTimeStrongGame_eq_prfOneTimeGame] + exact prfOneTimeGame_ofProbComp_le hh hε family query forge + +end PRFPad + /-! ### Concrete Carter–Wegman instantiations -/ section Instantiations @@ -735,6 +979,31 @@ theorem counterStrongGame_linearHash_le (n m : ℕ) simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat] using counterStrongGame_le (BitString.LinearHash.isDeltaUniversalHash n m) forger +/-- **PRF-masked Boolean-matrix Carter–Wegman one-time MAC (`BitString.LinearHash.hash`)**: +hashing `n`-bit messages to `m`-bit tags with a uniform Boolean matrix and masking by a PRF +evaluation at security parameter `m` has real-valued one-time forgery probability at most +`(2 ^ m)⁻¹` plus the PRF distinguishing advantage of `prfPadDistinguisher test` at parameter +`m`. -/ +theorem prfOneTimeGame_linearHash_le (n m : ℕ) + (family : List Bool → List Bool → List Bool) + (forger : OneTimeForger (BitString n) (BitString m)) + (test : (k : ℕ) → BitString k → ProbComp Bool) + (htest : ∀ r, + padDistinguisher (PMF.uniformOfFintype (Fin m → BitString n)) + BitString.LinearHash.hash forger r = ProbComp.eval (test m r)) : + (prfOneTimeGame (PMF.uniformOfFintype (Fin m → BitString n)) family m + BitString.LinearHash.hash forger true).toReal ≤ + ((2 : ℝ) ^ m)⁻¹ + + (Game.advantage + (ProbComp.eval (prfRealGame family (prfPadDistinguisher test) m)) + (ProbComp.eval (prfIdealGame (prfPadDistinguisher test) m)) : ℝ) := by + have hε : ((Fintype.card (BitString m) : ℝ≥0∞))⁻¹ ≠ ⊤ := by + simp + have h := prfOneTimeGame_le (BitString.LinearHash.isDeltaUniversalHash n m) hε family forger + test htest + simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat, ENNReal.toReal_inv, + ENNReal.toReal_pow, ENNReal.toReal_ofNat] using h + /-- **Subset-sum Carter–Wegman one-time MAC (`BitString.LinearHash` / `BitString.SubsetSum.hash`)**: hashing binary words `ι → Bool` into a finite additive abelian group `G` via uniform subset-sum weights has adaptive one-time forgery probability at most `1 / |G|`. -/ diff --git a/ComplexityTests/Crypto/CarterWegman.lean b/ComplexityTests/Crypto/CarterWegman.lean index 91f8db89b7..602db33232 100644 --- a/ComplexityTests/Crypto/CarterWegman.lean +++ b/ComplexityTests/Crypto/CarterWegman.lean @@ -19,7 +19,7 @@ and audits the axiom dependencies of the headline theorems in namespace ComplexityTests.Crypto.CarterWegman -open Cslib Cslib.Probability Cslib.Crypto.Protocols.CarterWegman +open Cslib Cslib.Probability Cslib.Crypto Cslib.Crypto.Protocols.CarterWegman open scoped ENNReal instance : Fact (Nat.Prime 7) := ⟨by decide⟩ @@ -116,6 +116,103 @@ example (padDist : PMF (ZMod 7)) : sampleOneTimeForger exact ENNReal.div_ne_top (by simp) (by simp) +-- Concrete `ProbComp` one-time forger and PRF-masked Carter–Wegman bound over `BitString 2`. +noncomputable def sampleBitStringQuery : ProbComp (BitString 2) := + pure (fun _ => false) + +noncomputable def sampleBitStringForge (_ : BitString 2) (t : BitString 2) : + ProbComp (BitString 2 × BitString 2) := + pure (fun _ => true, t) + +example (family : List Bool → List Bool → List Bool) : + (prfOneTimeGame (ProbComp.eval (ProbComp.uniform (Fin 2 → BitString 2))) + family 2 BitString.LinearHash.hash + (OneTimeForger.ofProbComp sampleBitStringQuery sampleBitStringForge) true).toReal ≤ + (((Fintype.card (BitString 2) : ℝ≥0∞))⁻¹).toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family + (prfPadDistinguisher fun _ r => + probPadTest (ProbComp.uniform (Fin 2 → BitString 2)) + BitString.LinearHash.hash sampleBitStringQuery sampleBitStringForge + (BitString.ofList 2 (List.ofFn r))) 2)) + (ProbComp.eval (prfIdealGame + (prfPadDistinguisher fun _ r => + probPadTest (ProbComp.uniform (Fin 2 → BitString 2)) + BitString.LinearHash.hash sampleBitStringQuery sampleBitStringForge + (BitString.ofList 2 (List.ofFn r))) 2)) : ℝ) := by + refine prfOneTimeGame_ofProbComp_le ?_ (by simp) family + sampleBitStringQuery sampleBitStringForge + simpa only [ProbComp.eval_uniform] using BitString.LinearHash.isDeltaUniversalHash 2 2 + +example (family : List Bool → List Bool → List Bool) : + (prfOneTimeStrongGame (ProbComp.eval (ProbComp.uniform (Fin 2 → BitString 2))) + family 2 BitString.LinearHash.hash + (OneTimeForger.ofProbComp sampleBitStringQuery sampleBitStringForge) true).toReal ≤ + (((Fintype.card (BitString 2) : ℝ≥0∞))⁻¹).toReal + + (Game.advantage + (ProbComp.eval (prfRealGame family + (prfPadDistinguisher fun _ r => + probPadTest (ProbComp.uniform (Fin 2 → BitString 2)) + BitString.LinearHash.hash sampleBitStringQuery sampleBitStringForge + (BitString.ofList 2 (List.ofFn r))) 2)) + (ProbComp.eval (prfIdealGame + (prfPadDistinguisher fun _ r => + probPadTest (ProbComp.uniform (Fin 2 → BitString 2)) + BitString.LinearHash.hash sampleBitStringQuery sampleBitStringForge + (BitString.ofList 2 (List.ofFn r))) 2)) : ℝ) := by + refine prfOneTimeStrongGame_ofProbComp_le ?_ (by simp) family + sampleBitStringQuery sampleBitStringForge + simpa only [ProbComp.eval_uniform] using BitString.LinearHash.isDeltaUniversalHash 2 2 + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le_add_advantage' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le_add_advantage + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfPadDistinguisher' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfPadDistinguisher + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le + +/-- +info: 'Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_linearHash_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_linearHash_le + /-- info: 'Cslib.Crypto.Protocols.CarterWegman.bind_uniform_sign' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ROADMAP.md b/ROADMAP.md index 92154191d3..b9ab50f8c8 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -579,7 +579,7 @@ developments, not assertions that every prerequisite is missing or assignments t | Algebraic and arithmetic complexity | Build on [VP and p-projections](Complexity/Computability/Circuit/Arithmetic/VP.lean), [VNP and VP ⊆ VNP](Complexity/Computability/Circuit/Arithmetic/VNP.lean), [determinant ∈ VP](Complexity/Computability/Circuit/Arithmetic/Determinant.lean) over commutative rings, and [Laplace expansion of the permanent](Complexity/Foundations/Data/Matrix/Permanent.lean). Prove permanent VNP-completeness with its characteristic assumptions, prove the Kabanets–Impagliazzo theorem, extend formula/branching-program models, identity testing, hitting sets, tensor and rank methods, and certify uniform construction costs separately from gate counts. | | Approximation and constraint satisfaction | [Random assignment](Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean) proves the `7 / 8` random-assignment bound for exact 3-CNF with three distinct variables per clause (`CNF.IsExactThreeDistinct`), and [Håstad's 3-bit test](Complexity/Computability/PCP/Approximation/Hastad.lean) proves completeness and soundness of Håstad's 3-bit linear test against `GapLabelCover` (`1 - δ` vs `1 / 2 + 4 * ε`). Build the reduction to MAX-E3LIN and, via the 4-clause XOR gadget, to MAX-E3SAT on clauses with three distinct variables, Raz's parallel repetition theorem, and the perfect-completeness `(1, 7 / 8 + ε)` reduction; develop further gap and approximation-preserving reductions, APX/PTAS/FPTAS, canonical inapproximability consequences of PCP, CSP classifications and relaxation gaps. State assumptions such as the Unique Games Conjecture explicitly. | | Pseudorandomness and coding | Build on [conditional `P = BPP` from exponential worst-case hardness in `E` (Impagliazzo–Wigderson)](Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean) via Nisan–Wigderson and Sudan–Trevisan–Vadhan, [Sudan's Reed–Solomon list decoding](Complexity/Foundations/Data/Code/Sudan.lean) (decoder correctness only: the decoder is noncomputable and no running time is claimed), and [expander-walk hitting bounds](Complexity/Foundations/Combinatorics/Expander/Hitting.lean). Extend space-bounded generators, extractors/condensers, limited independence, explicit expanders, and Guruswami–Sudan / local decoding. Separate finite combinatorial guarantees from uniform construction and decoding costs. | -| Complexity-theoretic cryptography | One-way functions imply SAT ∉ P and SAT ∉ BPP, and MCSP ∈ BPP rules them out (Kabanets–Cai; [OneWay/MCSP](Complexity/Crypto/Computational/OneWay/MCSP.lean)). [Naor bit commitments](Complexity/Crypto/Computational/Commitment.lean) (with hiding against randomized stateful PPT receivers and deterministic polynomial-time receiver-string/bit families), [Goldreich–Micali–Wigderson zero knowledge for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (uniform zero knowledge over deterministic polynomial-time instance/witness/auxiliary-input families via a 3-copy masked-3SAT truth-table commitment protocol), [uniform symmetric MACs and PRF-based MACs](Complexity/Crypto/Computational/MAC.lean) (`SUFCMA`, `EUFCMA`, `OneTimeEUFCMA`, quantitative `EUF-CMA ≤ SUF-CMA`, unique-tag equivalence, and the Boneh–Shoup Theorem 6.2 PRF-to-SUF-CMA/EUF-CMA reduction), and [keyed collision-resistant hash families and the Merkle–Damgård transform](Complexity/Crypto/Computational/CollisionResistant.lean) are proved. Uniform one-way functions are also equivalent to one-time secure digital signatures for `n`-bit messages, via [Lamport's construction](Complexity/Crypto/Computational/OneWayToSignature.lean); full EUF-CMA security implies one-way functions. [Carter–Wegman MACs](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) formalize unconditional one-time and adaptive multi-query issued-counter EUF-CMA/SUF-CMA security (`≤ ε`) from `ε`-almost-Δ-universal hash families together with the arbitrary-pad hybrid decomposition and `xpolyHash`/Boolean-matrix/subset-sum instantiations (computational PRF-pad security and fresh-counter nonces remain open). Extend the existing OWF/PRG/PRF/MAC/CRHF/commitment/ZK results with reusable adaptive reductions, many-time digital signatures, encryption, universal-instance zero knowledge, hard-core and hardness-amplification methods, and connections to learning and average-case hardness. | +| Complexity-theoretic cryptography | One-way functions imply SAT ∉ P and SAT ∉ BPP, and MCSP ∈ BPP rules them out (Kabanets–Cai; [OneWay/MCSP](Complexity/Crypto/Computational/OneWay/MCSP.lean)). [Naor bit commitments](Complexity/Crypto/Computational/Commitment.lean) (with hiding against randomized stateful PPT receivers and deterministic polynomial-time receiver-string/bit families), [Goldreich–Micali–Wigderson zero knowledge for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (uniform zero knowledge over deterministic polynomial-time instance/witness/auxiliary-input families via a 3-copy masked-3SAT truth-table commitment protocol), [uniform symmetric MACs and PRF-based MACs](Complexity/Crypto/Computational/MAC.lean) (`SUFCMA`, `EUFCMA`, `OneTimeEUFCMA`, quantitative `EUF-CMA ≤ SUF-CMA`, unique-tag equivalence, and the Boneh–Shoup Theorem 6.2 PRF-to-SUF-CMA/EUF-CMA reduction), and [keyed collision-resistant hash families and the Merkle–Damgård transform](Complexity/Crypto/Computational/CollisionResistant.lean) are proved. Uniform one-way functions are also equivalent to one-time secure digital signatures for `n`-bit messages, via [Lamport's construction](Complexity/Crypto/Computational/OneWayToSignature.lean); full EUF-CMA security implies one-way functions. [Carter–Wegman MACs](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) formalize unconditional one-time and adaptive multi-query issued-counter EUF-CMA/SUF-CMA security (`≤ ε`) from `ε`-almost-Δ-universal hash families together with the arbitrary-pad and PRF-masked hybrid bounds (`prfOneTimeGame_le`) and `xpolyHash`/Boolean-matrix/subset-sum instantiations (fresh-counter nonces remain open). Extend the existing OWF/PRG/PRF/MAC/CRHF/commitment/ZK results with reusable adaptive reductions, many-time digital signatures, encryption, universal-instance zero knowledge, hard-core and hardness-amplification methods, and connections to learning and average-case hardness. | | Communication, queries and data structures | Build on the `Ω(n)` bounded-error randomized disjointness lower bound ([Disjointness](Complexity/Computability/Communication/Disjointness.lean)), Karchmer–Wigderson ([Boolean](Complexity/Computability/Circuit/Boolean/KarchmerWigderson.lean), [monotone](Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean)), and Raz–Wigderson's monotone depth bound for bipartite matching ([BipartiteMatching](Complexity/Computability/Circuit/Monotone/BipartiteMatching.lean)). Extend multiparty protocols, discrepancy and information complexity, direct-sum/product results, lifting theorems, and reductions to streaming, sketching and cell-probe lower bounds. Reuse upstream query models. | | Proof complexity | Build on [Cook–Reckhow systems and simulations](Complexity/Computability/Complexity/ProofSystem.lean), including the polynomially bounded-system characterization of NP = coNP, the [resolution size–width tradeoff](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution/DPLL search-tree certificates](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin formulas on expanders](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean) and [Haken's pigeonhole lower bound](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean). Extend proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares. The certificate correspondence does not certify a DPLL solver's runtime. | | Average-case complexity and learning | Uniform-distribution learning on CSLib's PAC API, the LMN low-degree algorithm and Kushilevitz–Mansour with membership queries are [proved](Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean); running times are not machine-certified. Distributional problems and reductions, samplability, average-to-worst-case connections, PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Existing cryptographic learners are starting points, not coverage of learning theory. | @@ -1202,8 +1202,7 @@ Jukna coverage below is an additional target beyond the V1 port: quantitative nonnegligible CCA advantage lower bound against `idealStrongGame` as the block size grows, and the 4-round information-theoretic bidirectional random-round collision bound. Open: the leftover hash lemma stated over `ε`-universal families, with `IsTwoUniversal` as its - `1 / |Y|` case and the pseudoentropy clients updated, and Carter–Wegman MACs from Δ-universal - hashing. + `1 / |Y|` case and the pseudoentropy clients updated. * **Sigma protocols, Schnorr identification and Fiat–Shamir (#581).** Boneh–Shoup Chapter 19. The exact algebraic core is proved: [Sigma protocols](Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean) with explicit @@ -1270,14 +1269,16 @@ Jukna coverage below is an additional target beyond the V1 port: The design is on #643, and the TQBF, PCP and GMW bridges are recorded there. * **Classic symmetric constructions (#640, track D).** Proved: PRF-based MACs (#677), keyed - collision-resistant hash families and Merkle–Damgård (#678), universal hashing (#663), and the - Even–Mansour cipher in the ideal-permutation model (algebraic permutations, one-query secrecy, - one-sided query security, 2-query breaks when omitting either whitening key, and the Boneh–Shoup - Theorem 4.10 bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, #761). + collision-resistant hash families and Merkle–Damgård (#678), universal hashing (#663), + [Carter–Wegman MACs from Δ-universal hashing](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) + (#736, including one-time, adaptive multi-query issued-counter, and PRF-masked one-time bounds), + and the Even–Mansour cipher in the ideal-permutation model (algebraic permutations, one-query + secrecy, one-sided query security, 2-query breaks when omitting either whitening key, and the + Boneh–Shoup Theorem 4.10 bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, #761). Open: lazy-sampled bidirectional random-permutation coupling connecting the Even–Mansour bad-key intersection bound to full two-sided `Game.advantage`, Luby–Rackoff (three Feistel rounds over a - PRF give a PRP, four give a strong PRP), strongly unforgeable MACs and Carter–Wegman MACs from - Δ-universal hashing, and the Naor–Reingold PRF from the decisional Diffie–Hellman assumption. + PRF give a PRP, four give a strong PRP), and the Naor–Reingold PRF from the decisional + Diffie–Hellman assumption. * **Lattice Sigma protocols and post-quantum signatures (#640, track B).** Proved (#645): the [SIS hypothesis](Complexity/Crypto/Computational/SIS/Basic.lean) for power-of-two moduli, exact From 72cde54934d337d9c6be8b448e524bc7bb6230e5 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 17:55:25 +0000 Subject: [PATCH 2/2] fix(crypto): clarify single-query fixed-nonce PRF-pad reduction scope and review feedback (#736) --- .../Crypto/Protocols/MAC/CarterWegman.lean | 112 ++++++++++-------- ComplexityTests/Crypto/CarterWegman.lean | 34 ++++++ ROADMAP.md | 19 +-- 3 files changed, 110 insertions(+), 55 deletions(-) diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index 2aa28efecd..773e9197e3 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -63,17 +63,24 @@ This module formalizes: Unissued counter indices (`pads[idx]? = none`) are rejected (`false`), so zero-query success in the issued-counter games is `0` (whereas the standalone `zeroQueryGame` has success `1 / |Y|`); a fresh-counter experiment that accepts unissued nonces against fresh pads is separate scope. -5. **Arbitrary-pad and PRF-masked hybrid decomposition (`maskedOneTimeGame`, `padDistinguisher`, - `maskedOneTimeGame_toReal_le`, `maskedOneTimeGame_toReal_le_add_advantage`, `prfPadDist`, - `prfOneTimeGame`, `prfOneTimeStrongGame`, `prfPadDistinguisher`, `prfOneTimeGame_le`, +5. **Arbitrary-pad hybrid decomposition and the one-query, fixed-nonce PRF-pad reduction + (`maskedOneTimeGame`, `padDistinguisher`, `maskedOneTimeGame_toReal_le`, + `maskedOneTimeGame_toReal_le_add_advantage`, `prfPadDist`, `prfOneTimeGame`, + `prfOneTimeStrongGame`, `prfPadDistinguisher`, `prfOneTimeGame_le`, `prfOneTimeStrongGame_le`, `prfOneTimeGame_ofProbComp_le`)**: replacing the uniform pad `r ← PMF.uniformOfFintype Y` with any pad distribution `padDist : PMF Y` bounds the real forgery probability by `ε.toReal` plus the distinguishing advantage of `padDistinguisher` between - `padDist` and `PMF.uniformOfFintype Y` ([BonehShoup2023], Theorem 7.4). When `Y = BitString n` - and the pad is generated by evaluating a PRF family `family` at `List.replicate n false` under a - uniform `n`-bit key (`prfPadDist family n`), the single-query `OracleDistinguisher` adapter - `prfPadDistinguisher` connects the real and ideal pad experiments directly to `prfRealGame` and - `prfIdealGame`, bounding one-time forgery probability by `ε.toReal` plus the PRF advantage. + `padDist` and `PMF.uniformOfFintype Y` (after [BonehShoup2023], Section 7.4). In the one-query, + fixed-nonce case (after [BonehShoup2023], Section 7.4) where `Y = BitString n` and the pad is + generated by evaluating `family` at the fixed nonce `List.replicate n false` under a uniform + `n`-bit key (`prfPadDist family n`), the single-query `OracleDistinguisher` adapter + `prfPadDistinguisher` realizes the real and ideal pad experiments inside `prfRealGame` and + `prfIdealGame` at each parameter `n`, giving an exact single-query reduction that bounds + one-time forgery probability by `ε.toReal` plus the concrete PRF distinguishing advantage at + `n`. Certifying `IsOraclePPT encBool` admissibility of `prfPadDistinguisher` for uniform + word-level forger and hash families, deriving the asymptotic negligible-advantage corollary from + `PseudorandomFunction family`, and treating the many-time fresh-nonce PRF-masked Carter–Wegman + MAC of [BonehShoup2023], Section 7.4 remain open. 6. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash`, bound `2⁻ᵐ`), subset-sum hashing (`BitString.SubsetSum.hash`, bound `1 / |G|`), and pairwise independent @@ -100,8 +107,8 @@ This module formalizes: * `Cslib.Crypto.Protocols.CarterWegman.prfPadDist`, `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame`, `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame`, - `Cslib.Crypto.Protocols.CarterWegman.prfPadDistinguisher`: PRF-masked one-time Carter–Wegman - experiments and the single-query `OracleDistinguisher` adapter. + `Cslib.Crypto.Protocols.CarterWegman.prfPadDistinguisher`: one-query, fixed-nonce PRF-masked + Carter–Wegman experiments and the single-query `OracleDistinguisher` adapter. ## Main results @@ -122,8 +129,9 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher`, `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le`, `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le`, - `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le`: PRF-masked one-time - Carter–Wegman security (Boneh–Shoup Theorem 7.4). + `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le`: exact single-query reduction + to `prfRealGame`/`prfIdealGame` in the one-query, fixed-nonce case (after Boneh–Shoup + Section 7.4). * `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le`, `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_linearHash_le`, @@ -139,7 +147,7 @@ This module formalizes: * [M. N. Wegman, J. L. Carter, *New Hash Functions and Their Use in Authentication and Set Equality*][WegmanCarter1981] * [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, - Version 0.6][BonehShoup2023], Section 7.4 (Theorems 7.3 and 7.4). + Version 0.6][BonehShoup2023], Section 7.4. -/ @[expose] public section @@ -613,7 +621,7 @@ theorem counterStrongGame_le {seed : PMF K} {hash : K → M → Y} {ε : ℝ≥0 end Counter -/-! ### Pseudorandom-pad hybrid decomposition (Boneh–Shoup Theorem 7.4) -/ +/-! ### Pseudorandom-pad hybrid decomposition (after Boneh–Shoup Section 7.4) -/ section MaskedPad @@ -674,7 +682,7 @@ theorem maskedOneTimeGame_eq_bind_padDistinguisher (seed : PMF K) (padDist : PMF padDist.bind (padDistinguisher seed hash forger) := PMF.bind_comm seed padDist _ -/-- **Pseudorandom-pad Carter–Wegman bound** ([BonehShoup2023], Section 7.4, Theorem 7.4): +/-- **Pseudorandom-pad Carter–Wegman bound** (after [BonehShoup2023], Section 7.4): if `hash` is `ε`-almost-Δ-universal (`ε ≠ ⊤`), then the real-valued forgery probability under any pad distribution `padDist : PMF Y` is bounded by `ε.toReal` plus the distinguishing gap of `padDistinguisher` between `padDist` and `PMF.uniformOfFintype Y`. -/ @@ -694,8 +702,8 @@ theorem maskedOneTimeGame_toReal_le [Fintype Y] [Nonempty Y] {seed : PMF K} {has linarith [le_abs_self (((padDist.bind (padDistinguisher seed hash forger)) true).toReal - (oneTimeGame seed hash forger true).toReal)] -/-- `Game.advantage` form of `maskedOneTimeGame_toReal_le` ([BonehShoup2023], Section 7.4, -Theorem 7.4): the real-valued forgery probability under `padDist` is bounded by `ε.toReal` plus +/-- `Game.advantage` form of `maskedOneTimeGame_toReal_le` (after [BonehShoup2023], Section 7.4): +the real-valued forgery probability under `padDist` is bounded by `ε.toReal` plus `Game.advantage` between `padDist.bind (padDistinguisher seed hash forger)` and `(PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)`. -/ theorem maskedOneTimeGame_toReal_le_add_advantage [Fintype Y] [Nonempty Y] {seed : PMF K} @@ -745,7 +753,7 @@ theorem eval_probPadTest (seed : ProbComp K) (hash : K → M → Y) (query : Pro end MaskedPad -/-! ### PRF-masked one-time Carter–Wegman MAC (Boneh–Shoup Theorem 7.4) -/ +/-! ### One-query, fixed-nonce PRF-pad reduction (after Boneh–Shoup Section 7.4) -/ section PRFPad @@ -758,14 +766,15 @@ noncomputable def prfPadDist (family : List Bool → List Bool → List Bool) (n (BitString.uniformList n).map fun key => BitString.ofList n (family key (List.replicate n false)) -/-- The PRF-masked one-time Carter–Wegman EUF-CMA experiment ([BonehShoup2023], Section 7.4, -Theorem 7.4): the pad `r : BitString n` is generated by evaluating `family` on a uniform `n`-bit -PRF key at nonce `List.replicate n false`. -/ +/-- The one-query, fixed-nonce PRF-masked Carter–Wegman EUF-CMA experiment (after +[BonehShoup2023], Section 7.4): the pad `r : BitString n` is generated by evaluating `family` on a +uniform `n`-bit PRF key at the fixed nonce `List.replicate n false`. -/ noncomputable def prfOneTimeGame (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) : PMF Bool := maskedOneTimeGame seed (prfPadDist family n) hash forger -/-- The PRF-masked one-time Carter–Wegman SUF-CMA experiment. -/ +/-- The one-query, fixed-nonce PRF-masked Carter–Wegman SUF-CMA experiment (after +[BonehShoup2023], Section 7.4). -/ noncomputable def prfOneTimeStrongGame (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) : PMF Bool := @@ -779,9 +788,9 @@ theorem prfOneTimeStrongGame_eq_prfOneTimeGame (seed : PMF K) maskedOneTimeStrongGame_eq_maskedOneTimeGame seed (prfPadDist family n) hash forger /-- Single-query PRF `OracleDistinguisher` induced by a family of `ProbComp` pad tests -`test : (n : ℕ) → BitString n → ProbComp Bool`: at security parameter `n`, query the oracle once at +`test : (k : ℕ) → BitString k → ProbComp Bool`: at security parameter `n`, query the oracle once at the fixed nonce `List.replicate n false` and run `test n` on the `n`-bit view of the reply. -/ -def prfPadDistinguisher (test : (n : ℕ) → BitString n → ProbComp Bool) : +def prfPadDistinguisher (test : (k : ℕ) → BitString k → ProbComp Bool) : OracleDistinguisher := fun n _ => do let reply ← ProbOracleComp.query ((), List.replicate n false) ProbOracleComp.sample (test n (BitString.ofList n reply)) @@ -789,7 +798,7 @@ def prfPadDistinguisher (test : (n : ℕ) → BitString n → ProbComp Bool) : /-- In `prfRealGame`, `prfPadDistinguisher test` evaluates `test n` on a pad drawn from `prfPadDist family n`. -/ theorem eval_prfRealGame_prfPadDistinguisher (family : List Bool → List Bool → List Bool) - (test : (n : ℕ) → BitString n → ProbComp Bool) (n : ℕ) : + (test : (k : ℕ) → BitString k → ProbComp Bool) (n : ℕ) : ProbComp.eval (prfRealGame family (prfPadDistinguisher test) n) = (prfPadDist family n).bind (fun r => ProbComp.eval (test n r)) := by simp only [prfRealGame, prfPadDistinguisher, prfPadDist, ProbComp.eval_bind, @@ -800,14 +809,14 @@ theorem eval_prfRealGame_prfPadDistinguisher (family : List Bool → List Bool /-- Evaluating a uniformly random function `table : BitString n → BitString n` at any single point `x : BitString n` produces the uniform distribution on `BitString n`. -/ -theorem map_eval_uniformOfFintype_fun (n : ℕ) (x : BitString n) : +private theorem map_eval_uniformOfFintype_fun (n : ℕ) (x : BitString n) : (PMF.uniformOfFintype (BitString n → BitString n)).map (fun table => table x) = PMF.uniformOfFintype (BitString n) := by rw [← PMF.pi_uniformOfFintype, PMF.pi_map_eval] /-- In `prfIdealGame`, `prfPadDistinguisher test` evaluates `test n` on a uniform pad `r ← PMF.uniformOfFintype (BitString n)`. -/ -theorem eval_prfIdealGame_prfPadDistinguisher (test : (n : ℕ) → BitString n → ProbComp Bool) +theorem eval_prfIdealGame_prfPadDistinguisher (test : (k : ℕ) → BitString k → ProbComp Bool) (n : ℕ) : ProbComp.eval (prfIdealGame (prfPadDistinguisher test) n) = (PMF.uniformOfFintype (BitString n)).bind (fun r => ProbComp.eval (test n r)) := by @@ -820,10 +829,11 @@ theorem eval_prfIdealGame_prfPadDistinguisher (test : (n : ℕ) → BitString n funext table simp [randomFunctionOracle, show ProbComp.unifFin = OracleComp.query from rfl] -/-- **PRF-masked Carter–Wegman bound for an explicit `OracleDistinguisher`** -([BonehShoup2023], Section 7.4, Theorem 7.4): if `D` simulates `padDistinguisher seed hash forger` -in both `prfRealGame` and `prfIdealGame`, then the real-valued one-time forgery probability is at -most `ε.toReal` plus the PRF distinguishing advantage of `D`. -/ +/-- **Exact single-query PRF-pad reduction for an explicit `OracleDistinguisher`** in the +one-query, fixed-nonce case (after [BonehShoup2023], Section 7.4): if `D` simulates +`padDistinguisher seed hash forger` in both `prfRealGame` and `prfIdealGame` at parameter `n`, then +the real-valued one-time forgery probability is at most `ε.toReal` plus the concrete PRF +distinguishing advantage of `D` at `n`. -/ theorem prfOneTimeGame_le_of_distinguisher {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) @@ -840,15 +850,18 @@ theorem prfOneTimeGame_le_of_distinguisher {n : ℕ} {seed : PMF K} rw [hreal, hideal] exact maskedOneTimeGame_toReal_le_add_advantage hh hε (prfPadDist family n) forger -/-- **PRF-masked one-time Carter–Wegman EUF-CMA security** ([BonehShoup2023], Section 7.4, -Theorem 7.4): replacing the uniform pad `r ← PMF.uniformOfFintype (BitString n)` with the PRF pad -`prfPadDist family n` bounds the one-time forgery probability by `ε.toReal` plus the PRF -distinguishing advantage of `prfPadDistinguisher test`. -/ +/-- **Exact single-query PRF-pad reduction for `prfOneTimeGame`** in the one-query, fixed-nonce +case (after [BonehShoup2023], Section 7.4): replacing the uniform pad +`r ← PMF.uniformOfFintype (BitString n)` with the fixed-nonce PRF pad `prfPadDist family n` bounds +the real-valued one-time forgery probability at parameter `n` by `ε.toReal` plus the concrete PRF +distinguishing advantage of `prfPadDistinguisher test` between `prfRealGame` and `prfIdealGame`. +Admissibility (`IsOraclePPT encBool`) and the asymptotic corollary from +`PseudorandomFunction family` are not asserted here. -/ theorem prfOneTimeGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) - (test : (n : ℕ) → BitString n → ProbComp Bool) + (test : (k : ℕ) → BitString k → ProbComp Bool) (htest : ∀ r, padDistinguisher seed hash forger r = ProbComp.eval (test n r)) : (prfOneTimeGame seed family n hash forger true).toReal ≤ ε.toReal + @@ -861,13 +874,14 @@ theorem prfOneTimeGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString · rw [eval_prfIdealGame_prfPadDistinguisher] congr 1; funext r; exact (htest r).symm -/-- **PRF-masked one-time Carter–Wegman SUF-CMA security** ([BonehShoup2023], Section 7.4, -Theorem 7.4). -/ +/-- **Exact single-query PRF-pad reduction for `prfOneTimeStrongGame`** in the one-query, +fixed-nonce case (after [BonehShoup2023], Section 7.4); admissibility (`IsOraclePPT encBool`) and +the asymptotic `PseudorandomFunction` corollary are not asserted here. -/ theorem prfOneTimeStrongGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) - (test : (n : ℕ) → BitString n → ProbComp Bool) + (test : (k : ℕ) → BitString k → ProbComp Bool) (htest : ∀ r, padDistinguisher seed hash forger r = ProbComp.eval (test n r)) : (prfOneTimeStrongGame seed family n hash forger true).toReal ≤ ε.toReal + @@ -877,9 +891,11 @@ theorem prfOneTimeStrongGame_le {n : ℕ} {seed : PMF K} {hash : K → M → Bit rw [prfOneTimeStrongGame_eq_prfOneTimeGame] exact prfOneTimeGame_le hh hε family forger test htest -/-- **PRF-masked one-time Carter–Wegman bound for `ProbComp` samplers and forgers**: -any `ProbComp` hash-key sampler `seed`, query program `query`, and forgery program `forge` -automatically induce the single-query PRF distinguisher via `probPadTest`. -/ +/-- **Exact single-query PRF-pad reduction for `ProbComp` samplers and forgers** in the one-query, +fixed-nonce case (after [BonehShoup2023], Section 7.4): at parameter `n`, any `ProbComp` hash-key +sampler `seed`, query program `query`, and forgery program `forge` induce the single-query PRF +distinguisher via `probPadTest`, without asserting `IsOraclePPT encBool` admissibility or an +asymptotic `PseudorandomFunction` corollary. -/ theorem prfOneTimeGame_ofProbComp_le {n : ℕ} {seed : ProbComp K} {hash : K → M → BitString n} {ε : ℝ≥0∞} (hh : IsDeltaUniversalHash (ProbComp.eval seed) hash ε) (hε : ε ≠ ⊤) @@ -979,11 +995,13 @@ theorem counterStrongGame_linearHash_le (n m : ℕ) simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat] using counterStrongGame_le (BitString.LinearHash.isDeltaUniversalHash n m) forger -/-- **PRF-masked Boolean-matrix Carter–Wegman one-time MAC (`BitString.LinearHash.hash`)**: -hashing `n`-bit messages to `m`-bit tags with a uniform Boolean matrix and masking by a PRF -evaluation at security parameter `m` has real-valued one-time forgery probability at most -`(2 ^ m)⁻¹` plus the PRF distinguishing advantage of `prfPadDistinguisher test` at parameter -`m`. -/ +/-- **Exact single-query PRF-pad reduction for Boolean-matrix Carter–Wegman +(`BitString.LinearHash.hash`)** in the one-query, fixed-nonce case (after [BonehShoup2023], +Section 7.4): hashing `n`-bit messages to `m`-bit tags with a uniform Boolean matrix and masking by +a fixed-nonce PRF evaluation at security parameter `m` has real-valued one-time forgery probability +at most `(2 ^ m)⁻¹` plus the concrete PRF distinguishing advantage of `prfPadDistinguisher test` at +parameter `m` (without asserting `IsOraclePPT encBool` admissibility or an asymptotic +`PseudorandomFunction` corollary). -/ theorem prfOneTimeGame_linearHash_le (n m : ℕ) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger (BitString n) (BitString m)) diff --git a/ComplexityTests/Crypto/CarterWegman.lean b/ComplexityTests/Crypto/CarterWegman.lean index 602db33232..65e8e0bba5 100644 --- a/ComplexityTests/Crypto/CarterWegman.lean +++ b/ComplexityTests/Crypto/CarterWegman.lean @@ -164,6 +164,40 @@ example (family : List Bool → List Bool → List Bool) : sampleBitStringQuery sampleBitStringForge simpa only [ProbComp.eval_uniform] using BitString.LinearHash.isDeltaUniversalHash 2 2 +/-- Constant (insecure) PRF family that ignores its key and echoes the query word (so on the fixed +nonce `List.replicate n false` it always returns `0ⁿ`). -/ +def insecureZeroFamily (_key query : List Bool) : List Bool := query + +-- Concrete semantic check: under `insecureZeroFamily`, `prfPadDist` collapses to a point mass. +theorem prfPadDist_insecureZeroFamily (n : ℕ) : + prfPadDist insecureZeroFamily n = + PMF.pure (BitString.ofList n (List.replicate n false)) := + PMF.map_const (BitString.uniformList n) (BitString.ofList n (List.replicate n false)) + +-- Concrete semantic check: a pad test that checks whether the pad equals the fixed all-false pad +-- succeeds with probability `1` in `prfRealGame` against `insecureZeroFamily`. +example : + ProbComp.eval + (prfRealGame insecureZeroFamily + (prfPadDistinguisher fun k (r : BitString k) => + pure (decide (r = BitString.ofList k (List.replicate k false)))) 2) + true = 1 := by + rw [eval_prfRealGame_prfPadDistinguisher, prfPadDist_insecureZeroFamily] + simp + +-- Concrete semantic check: when the PRF pad is fixed (`insecureZeroFamily`) and the hash is +-- `fun _ _ => 0`, a forger querying `fun _ => false` and forging `(fun _ => true, pad)` wins +-- `prfOneTimeGame` with certainty (`PMF.pure true`). +example : + prfOneTimeGame (PMF.pure ()) insecureZeroFamily 2 + (fun (_ : Unit) (_ : BitString 2) => (0 : BitString 2)) + (OneTimeForger.ofProbComp sampleBitStringQuery sampleBitStringForge) = + PMF.pure true := by + rw [prfOneTimeGame, maskedOneTimeGame_eq_bind_padDistinguisher, prfPadDist_insecureZeroFamily] + simp only [padDistinguisher, OneTimeForger.ofProbComp, sampleBitStringQuery, sampleBitStringForge, + sign, verify, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.pure_bind, ProbComp.eval_pure] + congr 1 + /-- info: 'Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le_add_advantage' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ROADMAP.md b/ROADMAP.md index b9ab50f8c8..fd3e72f7ef 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -579,7 +579,7 @@ developments, not assertions that every prerequisite is missing or assignments t | Algebraic and arithmetic complexity | Build on [VP and p-projections](Complexity/Computability/Circuit/Arithmetic/VP.lean), [VNP and VP ⊆ VNP](Complexity/Computability/Circuit/Arithmetic/VNP.lean), [determinant ∈ VP](Complexity/Computability/Circuit/Arithmetic/Determinant.lean) over commutative rings, and [Laplace expansion of the permanent](Complexity/Foundations/Data/Matrix/Permanent.lean). Prove permanent VNP-completeness with its characteristic assumptions, prove the Kabanets–Impagliazzo theorem, extend formula/branching-program models, identity testing, hitting sets, tensor and rank methods, and certify uniform construction costs separately from gate counts. | | Approximation and constraint satisfaction | [Random assignment](Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean) proves the `7 / 8` random-assignment bound for exact 3-CNF with three distinct variables per clause (`CNF.IsExactThreeDistinct`), and [Håstad's 3-bit test](Complexity/Computability/PCP/Approximation/Hastad.lean) proves completeness and soundness of Håstad's 3-bit linear test against `GapLabelCover` (`1 - δ` vs `1 / 2 + 4 * ε`). Build the reduction to MAX-E3LIN and, via the 4-clause XOR gadget, to MAX-E3SAT on clauses with three distinct variables, Raz's parallel repetition theorem, and the perfect-completeness `(1, 7 / 8 + ε)` reduction; develop further gap and approximation-preserving reductions, APX/PTAS/FPTAS, canonical inapproximability consequences of PCP, CSP classifications and relaxation gaps. State assumptions such as the Unique Games Conjecture explicitly. | | Pseudorandomness and coding | Build on [conditional `P = BPP` from exponential worst-case hardness in `E` (Impagliazzo–Wigderson)](Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean) via Nisan–Wigderson and Sudan–Trevisan–Vadhan, [Sudan's Reed–Solomon list decoding](Complexity/Foundations/Data/Code/Sudan.lean) (decoder correctness only: the decoder is noncomputable and no running time is claimed), and [expander-walk hitting bounds](Complexity/Foundations/Combinatorics/Expander/Hitting.lean). Extend space-bounded generators, extractors/condensers, limited independence, explicit expanders, and Guruswami–Sudan / local decoding. Separate finite combinatorial guarantees from uniform construction and decoding costs. | -| Complexity-theoretic cryptography | One-way functions imply SAT ∉ P and SAT ∉ BPP, and MCSP ∈ BPP rules them out (Kabanets–Cai; [OneWay/MCSP](Complexity/Crypto/Computational/OneWay/MCSP.lean)). [Naor bit commitments](Complexity/Crypto/Computational/Commitment.lean) (with hiding against randomized stateful PPT receivers and deterministic polynomial-time receiver-string/bit families), [Goldreich–Micali–Wigderson zero knowledge for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (uniform zero knowledge over deterministic polynomial-time instance/witness/auxiliary-input families via a 3-copy masked-3SAT truth-table commitment protocol), [uniform symmetric MACs and PRF-based MACs](Complexity/Crypto/Computational/MAC.lean) (`SUFCMA`, `EUFCMA`, `OneTimeEUFCMA`, quantitative `EUF-CMA ≤ SUF-CMA`, unique-tag equivalence, and the Boneh–Shoup Theorem 6.2 PRF-to-SUF-CMA/EUF-CMA reduction), and [keyed collision-resistant hash families and the Merkle–Damgård transform](Complexity/Crypto/Computational/CollisionResistant.lean) are proved. Uniform one-way functions are also equivalent to one-time secure digital signatures for `n`-bit messages, via [Lamport's construction](Complexity/Crypto/Computational/OneWayToSignature.lean); full EUF-CMA security implies one-way functions. [Carter–Wegman MACs](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) formalize unconditional one-time and adaptive multi-query issued-counter EUF-CMA/SUF-CMA security (`≤ ε`) from `ε`-almost-Δ-universal hash families together with the arbitrary-pad and PRF-masked hybrid bounds (`prfOneTimeGame_le`) and `xpolyHash`/Boolean-matrix/subset-sum instantiations (fresh-counter nonces remain open). Extend the existing OWF/PRG/PRF/MAC/CRHF/commitment/ZK results with reusable adaptive reductions, many-time digital signatures, encryption, universal-instance zero knowledge, hard-core and hardness-amplification methods, and connections to learning and average-case hardness. | +| Complexity-theoretic cryptography | One-way functions imply SAT ∉ P and SAT ∉ BPP, and MCSP ∈ BPP rules them out (Kabanets–Cai; [OneWay/MCSP](Complexity/Crypto/Computational/OneWay/MCSP.lean)). [Naor bit commitments](Complexity/Crypto/Computational/Commitment.lean) (with hiding against randomized stateful PPT receivers and deterministic polynomial-time receiver-string/bit families), [Goldreich–Micali–Wigderson zero knowledge for NP](Complexity/Crypto/Computational/ZeroKnowledge.lean) (uniform zero knowledge over deterministic polynomial-time instance/witness/auxiliary-input families via a 3-copy masked-3SAT truth-table commitment protocol), [uniform symmetric MACs and PRF-based MACs](Complexity/Crypto/Computational/MAC.lean) (`SUFCMA`, `EUFCMA`, `OneTimeEUFCMA`, quantitative `EUF-CMA ≤ SUF-CMA`, unique-tag equivalence, and the Boneh–Shoup Theorem 6.2 PRF-to-SUF-CMA/EUF-CMA reduction), and [keyed collision-resistant hash families and the Merkle–Damgård transform](Complexity/Crypto/Computational/CollisionResistant.lean) are proved. Uniform one-way functions are also equivalent to one-time secure digital signatures for `n`-bit messages, via [Lamport's construction](Complexity/Crypto/Computational/OneWayToSignature.lean); full EUF-CMA security implies one-way functions. [Carter–Wegman MACs](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) formalize unconditional one-time and adaptive multi-query issued-counter EUF-CMA/SUF-CMA security (`≤ ε`) from `ε`-almost-Δ-universal hash families together with the arbitrary-pad hybrid bound, the exact single-query fixed-nonce reduction to `prfRealGame`/`prfIdealGame` (`prfOneTimeGame_le`, `prfOneTimeGame_ofProbComp_le`), and `xpolyHash`/Boolean-matrix/subset-sum instantiations (`IsOraclePPT` admissibility of the PRF-pad reduction, uniform word-level forger/hash families, the asymptotic `PseudorandomFunction` corollary, and fresh-counter nonces remain open). Extend the existing OWF/PRG/PRF/MAC/CRHF/commitment/ZK results with reusable adaptive reductions, many-time digital signatures, encryption, universal-instance zero knowledge, hard-core and hardness-amplification methods, and connections to learning and average-case hardness. | | Communication, queries and data structures | Build on the `Ω(n)` bounded-error randomized disjointness lower bound ([Disjointness](Complexity/Computability/Communication/Disjointness.lean)), Karchmer–Wigderson ([Boolean](Complexity/Computability/Circuit/Boolean/KarchmerWigderson.lean), [monotone](Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean)), and Raz–Wigderson's monotone depth bound for bipartite matching ([BipartiteMatching](Complexity/Computability/Circuit/Monotone/BipartiteMatching.lean)). Extend multiparty protocols, discrepancy and information complexity, direct-sum/product results, lifting theorems, and reductions to streaming, sketching and cell-probe lower bounds. Reuse upstream query models. | | Proof complexity | Build on [Cook–Reckhow systems and simulations](Complexity/Computability/Complexity/ProofSystem.lean), including the polynomially bounded-system characterization of NP = coNP, the [resolution size–width tradeoff](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution/DPLL search-tree certificates](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin formulas on expanders](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean) and [Haken's pigeonhole lower bound](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean). Extend proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares. The certificate correspondence does not certify a DPLL solver's runtime. | | Average-case complexity and learning | Uniform-distribution learning on CSLib's PAC API, the LMN low-degree algorithm and Kushilevitz–Mansour with membership queries are [proved](Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean); running times are not machine-certified. Distributional problems and reductions, samplability, average-to-worst-case connections, PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Existing cryptographic learners are starting points, not coverage of learning theory. | @@ -1271,13 +1271,16 @@ Jukna coverage below is an additional target beyond the V1 port: * **Classic symmetric constructions (#640, track D).** Proved: PRF-based MACs (#677), keyed collision-resistant hash families and Merkle–Damgård (#678), universal hashing (#663), [Carter–Wegman MACs from Δ-universal hashing](Complexity/Crypto/Protocols/MAC/CarterWegman.lean) - (#736, including one-time, adaptive multi-query issued-counter, and PRF-masked one-time bounds), - and the Even–Mansour cipher in the ideal-permutation model (algebraic permutations, one-query - secrecy, one-sided query security, 2-query breaks when omitting either whitening key, and the - Boneh–Shoup Theorem 4.10 bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, #761). - Open: lazy-sampled bidirectional random-permutation coupling connecting the Even–Mansour bad-key - intersection bound to full two-sided `Game.advantage`, Luby–Rackoff (three Feistel rounds over a - PRF give a PRP, four give a strong PRP), and the Naor–Reingold PRF from the decisional + (#736, including one-time, adaptive multi-query issued-counter, arbitrary-pad hybrid, and exact + single-query fixed-nonce `prfRealGame`/`prfIdealGame` reduction bounds), and the Even–Mansour + cipher in the ideal-permutation model (algebraic permutations, one-query secrecy, one-sided query + security, 2-query breaks when omitting either whitening key, and the Boneh–Shoup Theorem 4.10 + bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, #761). + Open: `IsOraclePPT` admissibility, uniform word-level forger/hash families, the asymptotic + `PseudorandomFunction` corollary, and fresh-nonce multi-query Carter–Wegman MAC security; + lazy-sampled bidirectional random-permutation coupling connecting the Even–Mansour bad-key + intersection bound to full two-sided `Game.advantage`; Luby–Rackoff (three Feistel rounds over a + PRF give a PRP, four give a strong PRP); and the Naor–Reingold PRF from the decisional Diffie–Hellman assumption. * **Lattice Sigma protocols and post-quantum signatures (#640, track B).** Proved (#645): the