Inversion from a predictor with partially uniform leakage

The inverter guesses the public hash value, fixes the predictor's other public and private randomness, and runs the shared Goldreich--Levin decoder. A short hash prefix is close to uniform on a fiber; guessing the remaining suffix loses only its cardinality. The unknown preimage and the split point occur only in the proof, never in the inverter.

These are finite reduction bounds. The hashed parity pair additionally needs a choice of split points, averaging over hash lengths and images, and a uniform PPT implementation.

Main definitions

• Cslib.Crypto.Pseudoentropy.guessInverter: guess the digest and run Goldreich–Levin.

Main results

• Cslib.Crypto.Pseudoentropy.correlation_le_guessInverter: prediction-to-inversion bound.
• Cslib.Probability.IsTwoUniversal.fiber_correlation_le_guessInverter: specialize to a uniform fiber without regularity assumptions.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, Lemma 4. We use decoder success as the nonnegative game score in Games 2--5, instead of maximizing signed prediction advantage over all preimages. This gives the same kind of polynomial loss.

Adapted from Crypto/Computational/Pseudoentropy/Reduction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the pinned finite-PMF distance and shared decoder.

noncomputable def Cslib.Crypto.Pseudoentropy.guessInverter {n : ℕ} {Image : Type u_1} {Seed : Type u_2} {Digest : Type u_3} [DecidableEq Image] [Fintype Digest] [Nonempty Digest] (f : BitString n → Image) (predictor : Seed → Digest → BitString n → Bool) (seed : PMF Seed) (precision : ℕ) (image : Image) : PMF (BitString n)

Guess the entire leakage and run the Goldreich–Levin decoder. Its behavior is independent of the prefix/suffix split used to analyze it. seed may include saved predictor coins.

theorem Cslib.Crypto.Pseudoentropy.guessInverter_equiv {n : ℕ} {Image : Type u_1} {Seed : Type u_2} {Digest : Type u_3} [DecidableEq Image] [Fintype Digest] [Nonempty Digest] {Other : Type u_4} [Fintype Other] [Nonempty Other] (f : BitString n → Image) (predictor : Seed → Digest → BitString n → Bool) (seed : PMF Seed) (precision : ℕ) (image : Image) (e : Other ≃ Digest) : guessInverter f (fun (s : Seed) (digest : Other) => predictor s (e digest)) seed precision image = guessInverter f predictor seed precision image

Re-encoding the guessed digest by an equivalence preserves the inverter exactly.

theorem Cslib.Crypto.Pseudoentropy.correlation_le_guessInverter {n : ℕ} {Image : Type u_1} {Seed : Type u_2} [DecidableEq Image] [Fintype Seed] {Prefix : Type u_4} {Suffix : Type u_5} [Fintype Prefix] [Fintype Suffix] [Nonempty Prefix] [Nonempty Suffix] (f : BitString n → Image) (image : Image) (source : PMF (BitString n)) (hsource : ∀ x ∈ source.support, f x = image) (predictor : Seed → Prefix × Suffix → BitString n → Bool) (seed : PMF Seed) (hash : Seed → BitString n → Prefix × Suffix) (precision : ℕ) (hp : 0 < precision) : ∑ s : Seed, (seed s).toReal * ∑ x : BitString n, (source x).toReal * (2 * GoldreichLevin.agreement (predictor s (hash s x)) x - 1) ≤ 1 / ↑precision + 4 * dist (Probability.seededHash seed source fun (s : Seed) (x : BitString n) => (hash s x).1) (seed.bind fun (s : Seed) => PMF.map (fun (x : Prefix) => (s, x)) (Probability.PMF.uniformOfFintype Prefix)) + 2 * ↑(Fintype.card Suffix) * ((PMF.map (fun (x : BitString n) => f x == image) (guessInverter f predictor seed precision image)) true).toReal

Guessing the leakage converts parity correlation into inversion success. Only its prefix must be statistically close to uniform; its suffix costs the number of possible guesses.

theorem Cslib.Probability.IsTwoUniversal.correlation_le_guessInverter {n : ℕ} {Image : Type u_1} {Seed : Type u_2} [DecidableEq Image] [Fintype Seed] {Prefix : Type u_4} {Suffix : Type u_5} [Fintype Prefix] [Fintype Suffix] [Nonempty Prefix] [Nonempty Suffix] (f : BitString n → Image) (image : Image) (source : PMF (BitString n)) (hsource : ∀ x ∈ source.support, f x = image) (predictor : Seed → Prefix × Suffix → BitString n → Bool) {seed : PMF Seed} {hash : Seed → BitString n → Prefix × Suffix} (hhash : IsTwoUniversal seed fun (s : Seed) (x : BitString n) => (hash s x).1) (precision : ℕ) (hp : 0 < precision) : ∑ s : Seed, (seed s).toReal * ∑ x : BitString n, (source x).toReal * (2 * Crypto.GoldreichLevin.agreement (predictor s (hash s x)) x - 1) ≤ 1 / ↑precision + 2 * √(↑(Fintype.card Prefix) * PMF.collisionProbability source) + 2 * ↑(Fintype.card Suffix) * ((PMF.map (fun (x : BitString n) => f x == image) (Crypto.Pseudoentropy.guessInverter f predictor seed precision image)) true).toReal

Universal hashing supplies the prefix error in the prediction-to-inversion bound.

theorem Cslib.Probability.IsTwoUniversal.fiber_correlation_le_guessInverter {n : ℕ} {Image : Type u_1} {Seed : Type u_2} [DecidableEq Image] [Fintype Seed] {Prefix : Type u_4} {Suffix : Type u_5} [Fintype Prefix] [Fintype Suffix] [Nonempty Prefix] [Nonempty Suffix] (f : BitString n → Image) (image : Image) [Nonempty { x : BitString n // f x = image }] (predictor : Seed → Prefix × Suffix → BitString n → Bool) {seed : PMF Seed} {hash : Seed → BitString n → Prefix × Suffix} (hhash : IsTwoUniversal seed fun (s : Seed) (x : BitString n) => (hash s x).1) (precision : ℕ) (hp : 0 < precision) : ∑ s : Seed, (seed s).toReal * ∑ x : { x : BitString n // f x = image }, ((PMF.uniformOfFintype { x : BitString n // f x = image }) x).toReal * (2 * Crypto.GoldreichLevin.agreement (predictor s (hash s ↑x)) ↑x - 1) ≤ 1 / ↑precision + 2 * √(↑(Fintype.card Prefix) / ↑(Nat.card { x : BitString n // f x = image })) + 2 * ↑(Fintype.card Suffix) * ((PMF.map (fun (x : BitString n) => f x == image) (Crypto.Pseudoentropy.guessInverter f predictor seed precision image)) true).toReal

On a uniform fiber, the extraction error depends on its size. No regularity assumption is made about the other fibers of the function.