Hard-core predicates and one-bit expansion

A hard-core predicate is efficiently computable from a seed but unpredictable from its image. Security quantifies over uniform PPT predictors and measures absolute bias from one half, so it also rules out reliable anticorrelation. This property alone does not require the image function to be one-way or injective.

The reduction appends a fixed trial bit to the image, runs a distinguisher, and predicts the trial on acceptance or its complement on rejection. The distinguishing gap is the average of the signed biases of the two fixed predictors. Both are single uniform programs, with no choice depending on the security parameter. Pr[p] is the probability, in the reals, that the program p returns true (the scoped notation of Cslib.Probability).

Appending a hard-core predicate to an efficient length-preserving permutation gives a one-bit PRG in the existing finite-family security API. This is conditional on the hard-core predicate; the Goldreich–Levin construction is a separate step in the OWP-to-PRG reduction.

Main definitions

• Cslib.Crypto.HardCore: efficient evaluation and uniform computational unpredictability.
• Cslib.Crypto.hardCorePredictor: the functional distinguishing-to-prediction reduction.

Main results

• Cslib.Crypto.hardCore_advantage_le: a concrete average-prediction-bias bound.
• Cslib.Crypto.HardCore.indistinguishable: replace a hidden predicate by an independent bit.
• Cslib.Crypto.OneWayPermutation.pseudorandomGenerator_of_hardCore: conditional one-bit PRG.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 9.
• L. Trevisan, CS276 Lecture 13: Pseudorandom Generators, scribed by Siu-On Chan, Theorem 2 and its prediction reduction.

Adapted from Crypto/Computational/HardCore.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared nonnegative game API and tidy machines.

noncomputable def Cslib.Crypto.predictionGame (f : List Bool → List Bool) (predicate : List Bool → Bool) (adversary : Distinguisher) (n : ℕ) : ProbComp Bool

Predict a predicate of a uniform seed, given only its image and the security parameter.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.predictionAdvantage (f : List Bool → List Bool) (predicate : List Bool → Bool) (adversary : Distinguisher) (n : ℕ) : NNReal

Absolute bias above or below the correctness probability of a fair guess.

structure Cslib.Crypto.HardCore (f : List Bool → List Bool) (predicate : List Bool → Bool) : Prop

A plain polynomial-time predicate whose value is computationally hidden by the image function.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime predicate Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool

  Computing the predicate from the seed uses a fixed polynomial-time machine.

• secure : Game.Indistinguishable (fun (adversary : Distinguisher) (n : ℕ) => (predictionGame f predicate adversary n).eval) (fun (x : Distinguisher) (x_1 : ℕ) => Probability.PMF.uniformOfFintype Bool) (Probability.IsPPT Turing.MultiTapeTM.encBool)

  A predictor's correctness is indistinguishable from a fair coin.

theorem Cslib.Crypto.hardCore_iff_tidy {f : List Bool → List Bool} {predicate : List Bool → Bool} : HardCore f predicate ↔ Turing.MultiTapeTM.ComputableTidilyInPolyTime predicate Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool ∧ Game.Indistinguishable (fun (adversary : Distinguisher) (n : ℕ) => (predictionGame f predicate adversary n).eval) (fun (x : Distinguisher) (x_1 : ℕ) => Probability.PMF.uniformOfFintype Bool) (Probability.IsPPT Turing.MultiTapeTM.encBool)

Recover the tidy presentation for proofs without changing the security contract.

theorem Cslib.Crypto.HardCore.unpredictable {f : List Bool → List Bool} {predicate : List Bool → Bool} (h : HardCore f predicate) (adversary : Distinguisher) (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Negligible (predictionAdvantage f predicate adversary)

The shared security property gives negligible absolute prediction bias.

theorem Cslib.Crypto.HardCore.of_unpredictable {f : List Bool → List Bool} {predicate : List Bool → Bool} (hp : Turing.MultiTapeTM.ComputableTidilyInPolyTime predicate Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) (h : ∀ (adversary : Distinguisher), Probability.IsPPT Turing.MultiTapeTM.encBool adversary → Negligible (predictionAdvantage f predicate adversary)) : HardCore f predicate

Establish a hard-core predicate from efficient evaluation and negligible prediction bias.

theorem Cslib.Crypto.isPPTOn_predictionGame {f : List Bool → List Bool} {predicate : List Bool → Bool} {adversary : Distinguisher} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hp : Turing.MultiTapeTM.ComputableTidilyInPolyTime predicate Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (predictionGame f predicate adversary)

The prediction experiment is a uniform PPT program when its ingredients are efficient.

def Cslib.Crypto.hardCorePredictor (adversary : Distinguisher) (trial : Bool) : Distinguisher

Use acceptance of an appended trial bit to predict the hidden predicate.

theorem Cslib.Crypto.isPPT_hardCorePredictor {adversary : Distinguisher} (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) (trial : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool (hardCorePredictor adversary trial)

The reduction charges for constructing the extended input and executing the distinguisher.

noncomputable def Cslib.Crypto.hardCoreIdeal (f : List Bool → List Bool) (n : ℕ) : PMF (List Bool)

The ideal hybrid replaces the hidden predicate by an independent fair bit.

theorem Cslib.Crypto.hardCore_gap (f : List Bool → List Bool) (predicate : List Bool → Bool) (adversary : Distinguisher) (n : ℕ) : ((prgRealGame (fun (seed : List Bool) => f seed ++ [predicate seed]) adversary n).eval true).toReal - ↑(distinguishingGame (hardCoreIdeal f n) (adversary n)).succProbability = (((predictionGame f predicate (hardCorePredictor adversary false) n).eval true).toReal + ((predictionGame f predicate (hardCorePredictor adversary true) n).eval true).toReal - 1) / 2

The distinguishing gap is the average signed bias of two fixed uniform predictors.

theorem Cslib.Crypto.hardCore_advantage_le (f : List Bool → List Bool) (predicate : List Bool → Bool) (adversary : Distinguisher) (n : ℕ) : Game.advantage (prgRealGame (fun (seed : List Bool) => f seed ++ [predicate seed]) adversary n).eval (distinguishingGame (hardCoreIdeal f n) (adversary n)) ≤ (predictionAdvantage f predicate (hardCorePredictor adversary false) n + predictionAdvantage f predicate (hardCorePredictor adversary true) n) / 2

Distinguishing the predicate from a fair bit costs at most the average prediction bias.

theorem Cslib.Crypto.HardCore.indistinguishable {f : List Bool → List Bool} {predicate : List Bool → Bool} (h : HardCore f predicate) : ComputationallyIndistinguishable (generatorEnsemble fun (seed : List Bool) => f seed ++ [predicate seed]) (hardCoreIdeal f)

A hard-core predicate can be replaced by an independent fair bit in every uniform PPT test.

theorem Cslib.Crypto.HardCore.indistinguishable_of_uniform {f : List Bool → List Bool} {predicate : List Bool → Bool} (h : HardCore f predicate) (huniform : ∀ (n : ℕ), PMF.map f (BitString.uniformList n) = BitString.uniformList n) : ComputationallyIndistinguishable (generatorEnsemble fun (seed : List Bool) => f seed ++ [predicate seed]) fun (n : ℕ) => BitString.uniformList (n + 1)

If the image function preserves uniform seeds, the ideal hybrid is uniform at length n+1.

theorem Cslib.Crypto.HardCore.pseudorandomGenerator {f : List Bool → List Bool} {predicate : List Bool → Bool} (h : HardCore f predicate) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlen : ∀ (word : List Bool), (f word).length = word.length) (huniform : ∀ (n : ℕ), PMF.map f (BitString.uniformList n) = BitString.uniformList n) : PseudorandomGenerator (fun (seed : List Bool) => f seed ++ [predicate seed]) fun (n : ℕ) => n + 1

An efficient length-preserving function that preserves uniform seeds gives a one-bit PRG when extended by a hard-core predicate. The later predicate construction uses one-wayness.

theorem Cslib.Crypto.OneWayPermutation.pseudorandomGenerator_of_hardCore {f : List Bool → List Bool} {predicate : List Bool → Bool} (hf : OneWayPermutation f) (h : HardCore f predicate) : PseudorandomGenerator (fun (seed : List Bool) => f seed ++ [predicate seed]) fun (n : ℕ) => n + 1

A one-way permutation with a hard-core predicate gives a uniform polynomial-time one-bit PRG.