The next-bit test

A generator G with m-bit outputs is unpredictable when no predictor, shown the first i bits of a generated output, guesses bit i with probability much better than 1 / 2 Boneh and Shoup, Attack Game 3.2 and Definition 3.3. This file proves that unpredictability is equivalent to security in the sense of Attack Game 3.1, up to a factor of m in the error. This is the next-bit theorem usually credited to Yao; the proof follows Boneh and Shoup, Section 3.5 (see also Arora and Barak, Chapter 9).

The proof is a hybrid argument. The k-th hybrid gives a test the first k bits of a generated output followed by uniform bits. Running the test on the 0-th hybrid is the ideal experiment of Attack Game 3.1 and running it on the m-th is the real experiment, so the difference of the two acceptance probabilities telescopes into the gaps between adjacent hybrids; the hybrids and the telescoping hold for outputs over any finite alphabet. The predictor for bit i built from a test pads the first i bits with a uniform candidate bit and uniform later bits, runs the test, and keeps the candidate if the test accepts and flips it otherwise. By the distinguisher/predictor lemma Boneh and Shoup, Lemma 3.5 it is correct with probability exactly 1 / 2 plus the i-th hybrid gap.

Here the position i is a parameter of the prediction game, whereas the adversary of Attack Game 3.2 chooses it. A predictor that chooses its position at random wins with the average of the fixed-position probabilities, so a bound for every fixed position also bounds it. As in the definition of Cslib.Crypto.PRG.Generator.Secure, admissible tests and predictors are given by caller-supplied predicates; the reductions between them are Cslib.Crypto.PRG.nextBitPredictor and Cslib.Crypto.PRG.predictionTest.

Main definitions

• Cslib.Crypto.PRG.guessOfDistinguisher: guess a bit with a randomized distinguisher.
• Cslib.Crypto.PRG.Generator.hybridDist, Cslib.Crypto.PRG.Generator.hybridExperiment, Cslib.Crypto.PRG.Generator.hybridGap: the hybrids between generated and uniform outputs.
• Cslib.Crypto.PRG.Generator.predictionExperiment, Cslib.Crypto.PRG.Generator.predictionAdvantage: Attack Game 3.2 at a fixed position.
• Cslib.Crypto.PRG.Generator.Unpredictable: concrete unpredictability against admissible predictors.
• Cslib.Crypto.PRG.nextBitPredictor: the predictor built from a test.
• Cslib.Crypto.PRG.nextBitGuess: the predictor built from a deterministic test, with its random choices fixed (Cslib.Crypto.PRG.nextBitPredictor_pure).
• Cslib.Crypto.PRG.predictionTest: the test built from a predictor.

Main results

• Cslib.Crypto.PRG.toReal_bind_guessOfDistinguisher: the distinguisher/predictor lemma.
• Cslib.Crypto.PRG.Generator.sum_hybridGap, Cslib.Crypto.PRG.Generator.exists_div_le_hybridGap: the hybrid gaps telescope, so one of them is at least the average.
• Cslib.Crypto.PRG.Generator.toReal_predictionExperiment_nextBitPredictor: the predictor built from a test is correct with probability 1 / 2 plus a hybrid gap.
• Cslib.Crypto.PRG.Generator.advantage_le_sum_predictionAdvantage, Cslib.Crypto.PRG.Generator.exists_half_add_div_le_predictionExperiment: a test with advantage ε yields a predictor for some position with success probability 1 / 2 + ε / m.
• Cslib.Crypto.PRG.Generator.Unpredictable.secure: unpredictability with error δ implies security with error m * δ.
• Cslib.Crypto.PRG.Generator.Secure.unpredictable: security with error ε implies unpredictability with error ε.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 3.5
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 9

noncomputable def Cslib.Crypto.PRG.guessOfDistinguisher (d : Bool → PMF Bool) : PMF Bool

Guess a bit with a randomized distinguisher d: draw a uniform candidate bit r, run d r, and output r if it accepts and !r if it rejects Boneh and Shoup, Lemma 3.5.

theorem Cslib.Crypto.PRG.toReal_bind_guessOfDistinguisher {S : Type u_1} (μ : PMF S) (target : S → Bool) (d : S → Bool → PMF Bool) : ((μ.bind fun (x : S) => PMF.map (fun (g : Bool) => decide (g = target x)) (guessOfDistinguisher (d x))) true).toReal = 1 / 2 + ((μ.bind fun (x : S) => d x (target x)) true).toReal - ((μ.bind fun (x : S) => (Probability.PMF.uniformOfFintype Bool).bind (d x)) true).toReal

The distinguisher/predictor lemma Boneh and Shoup, Lemma 3.5. Draw x from μ. The guess guessOfDistinguisher (d x) equals target x with probability 1 / 2, plus the probability that d x accepts target x, minus the probability that d x accepts an independent uniform bit.

noncomputable def Cslib.Crypto.PRG.Generator.hybridDist {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (k : ℕ) : PMF (Fin m → α)

The k-th hybrid: the first k symbols of the generator's output on a uniform seed, followed by independent uniform symbols. It is Hybrid m - k of Boneh and Shoup, Section 3.5.

@[simp]

theorem Cslib.Crypto.PRG.Generator.hybridDist_zero {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) : G.hybridDist 0 = Probability.PMF.uniformOfFintype (Fin m → α)

The 0-th hybrid is uniform.

theorem Cslib.Crypto.PRG.Generator.hybridDist_of_le {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) {k : ℕ} (hk : m ≤ k) : G.hybridDist k = G.outputDist

The k-th hybrid with m ≤ k is the output distribution of the generator.

noncomputable def Cslib.Crypto.PRG.Generator.hybridExperiment {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) (k : ℕ) : PMF Bool

Run a test on the k-th hybrid.

@[simp]

theorem Cslib.Crypto.PRG.Generator.hybridExperiment_zero {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) : G.hybridExperiment adversary 0 = idealExperiment adversary

A test run on the 0-th hybrid is the ideal experiment of Attack Game 3.1.

theorem Cslib.Crypto.PRG.Generator.hybridExperiment_of_le {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) {k : ℕ} (hk : m ≤ k) : G.hybridExperiment adversary k = G.realExperiment adversary

A test run on the k-th hybrid with m ≤ k is the real experiment of Attack Game 3.1.

theorem Cslib.Crypto.PRG.Generator.hybridExperiment_eq_bind {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) (k : ℕ) : G.hybridExperiment adversary k = G.outputDist.bind fun (y : Fin m → α) => (Probability.PMF.uniformOfFintype (Fin m → α)).bind fun (z : Fin m → α) => adversary fun (j : Fin m) => if ↑j < k then y j else z j

A test run on the k-th hybrid sees the first k symbols of a generated output followed by the remaining symbols of an independent uniform string.

noncomputable def Cslib.Crypto.PRG.Generator.hybridGap {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) (i : Fin m) : ℝ

The i-th hybrid gap of a test: the probability that it accepts the (i + 1)-st hybrid minus the probability that it accepts the i-th, in which symbol i is uniform instead of generated.

theorem Cslib.Crypto.PRG.Generator.sum_hybridGap {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) : ∑ i : Fin m, G.hybridGap adversary i = ((G.realExperiment adversary) true).toReal - ((idealExperiment adversary) true).toReal

The hybrid gaps of a test telescope to the probability that it accepts in the real experiment minus the probability that it accepts in the ideal experiment.

theorem Cslib.Crypto.PRG.Generator.exists_div_le_hybridGap {Seed : Type u_1} {α : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype α] [Nonempty α] {m : ℕ} (G : Generator Seed (Fin m → α)) (adversary : Adversary (Fin m → α)) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ ((G.realExperiment adversary) true).toReal - ((idealExperiment adversary) true).toReal) : ∃ (i : Fin m), ε / ↑m ≤ G.hybridGap adversary i

The hybrid argument. If 0 < m and a test accepts in the real experiment with probability at least ε more than in the ideal experiment, then one of its hybrid gaps is at least ε / m.

noncomputable def Cslib.Crypto.PRG.Generator.predictionExperiment {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : PMF Bool

Attack Game 3.2 of [BS23] at the fixed position i: the predictor receives the first i bits of the generator's output on a uniform seed, and the experiment outputs true exactly when the predictor's guess is bit i.

noncomputable def Cslib.Crypto.PRG.Generator.predictionAdvantage {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : ℝ

The advantage of a predictor in Attack Game 3.2 of [BS23]: the distance of its probability of guessing bit i correctly from 1 / 2.

def Cslib.Crypto.PRG.Generator.Unpredictable {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (Admissible : (i : Fin m) → Adversary (Fin ↑i → Bool) → Prop) (δ : NNReal) : Prop

Concrete unpredictability against admissible predictors Boneh and Shoup, Definition 3.3 with an explicit error: every admissible predictor for every position has advantage at most δ. As for Cslib.Crypto.PRG.Generator.Secure, the predicate Admissible is supplied by the caller; fun _ _ => True allows arbitrary predictors.

noncomputable def Cslib.Crypto.PRG.nextBitPredictor {m : ℕ} (adversary : Adversary (Fin m → Bool)) (i : Fin m) : Adversary (Fin ↑i → Bool)

The predictor for bit i built from a test, following the proof of Boneh and Shoup, Theorem 3.6. Given the first i bits x, it applies Cslib.Crypto.PRG.guessOfDistinguisher to the distinguisher that, on a candidate bit r, runs the test on x, followed by r at position i, followed by uniform bits.

def Cslib.Crypto.PRG.nextBitGuess {m : ℕ} (test : (Fin m → Bool) → Bool) (i : Fin m) (r : Bool) (u : Fin m → Bool) (x : Fin ↑i → Bool) : Bool

The guess of the predictor built from a deterministic test, with its random choices fixed. Given the first i bits x, it runs the test on x, followed by the candidate bit r at position i, followed by the bits of u after position i, and outputs r if the test accepts and !r otherwise.

theorem Cslib.Crypto.PRG.nextBitPredictor_pure {m : ℕ} (test : (Fin m → Bool) → Bool) (i : Fin m) (x : Fin ↑i → Bool) : nextBitPredictor (fun (y : Fin m → Bool) => PMF.pure (test y)) i x = do let r ← Probability.PMF.uniformOfFintype Bool PMF.map (fun (u : Fin m → Bool) => nextBitGuess test i r u x) (Probability.PMF.uniformOfFintype (Fin m → Bool))

For a deterministic test, the predictor built from it draws a uniform candidate bit r and a uniform string u and outputs nextBitGuess test i r u x.

theorem Cslib.Crypto.PRG.Generator.toReal_predictionExperiment_nextBitPredictor {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (adversary : Adversary (Fin m → Bool)) (i : Fin m) : ((G.predictionExperiment i (nextBitPredictor adversary i)) true).toReal = 1 / 2 + G.hybridGap adversary i

The predictor built from a test guesses bit i correctly with probability exactly 1 / 2 plus the i-th hybrid gap of the test.

theorem Cslib.Crypto.PRG.Generator.predictionAdvantage_nextBitPredictor {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (adversary : Adversary (Fin m → Bool)) (i : Fin m) : G.predictionAdvantage i (nextBitPredictor adversary i) = |G.hybridGap adversary i|

The advantage of the predictor built from a test is the absolute value of the corresponding hybrid gap.

theorem Cslib.Crypto.PRG.Generator.advantage_le_sum_predictionAdvantage {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (adversary : Adversary (Fin m → Bool)) : G.advantage adversary ≤ ∑ i : Fin m, G.predictionAdvantage i (nextBitPredictor adversary i)

The advantage of a test is at most the sum, over all positions, of the advantages of the predictors built from it.

theorem Cslib.Crypto.PRG.Generator.exists_div_le_predictionAdvantage {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (adversary : Adversary (Fin m → Bool)) (hm : 0 < m) : ∃ (i : Fin m), G.advantage adversary / ↑m ≤ G.predictionAdvantage i (nextBitPredictor adversary i)

If 0 < m, then for some position the predictor built from a test has advantage at least the advantage of the test divided by m.

theorem Cslib.Crypto.PRG.Generator.exists_half_add_div_le_predictionExperiment {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (adversary : Adversary (Fin m → Bool)) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ ((G.realExperiment adversary) true).toReal - ((idealExperiment adversary) true).toReal) : ∃ (i : Fin m), 1 / 2 + ε / ↑m ≤ ((G.predictionExperiment i (nextBitPredictor adversary i)) true).toReal

The next-bit theorem in the one-sided form of Arora and Barak, Chapter 9. If 0 < m and a test accepts in the real experiment with probability at least ε more than in the ideal experiment, then for some position i the predictor built from the test guesses bit i correctly with probability at least 1 / 2 + ε / m.

theorem Cslib.Crypto.PRG.Generator.Unpredictable.secure {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} {G : Generator Seed (Fin m → Bool)} {Admissible : Adversary (Fin m → Bool) → Prop} {AdmissiblePredictor : (i : Fin m) → Adversary (Fin ↑i → Bool) → Prop} {δ : NNReal} (hG : G.Unpredictable AdmissiblePredictor δ) (hred : ∀ (adversary : Adversary (Fin m → Bool)), Admissible adversary → ∀ (i : Fin m), AdmissiblePredictor i (nextBitPredictor adversary i)) : G.Secure Admissible (↑m * δ)

Unpredictability implies security Boneh and Shoup, Theorem 3.6. If every admissible predictor has advantage at most δ, and the predictors built from admissible tests are admissible, then every admissible test has advantage at most m * δ.

noncomputable def Cslib.Crypto.PRG.predictionTest {m : ℕ} (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : Adversary (Fin m → Bool)

The test built from a predictor for bit i, following the proof of Boneh and Shoup, Theorem 3.4: run the predictor on the first i bits and accept exactly when its guess is bit i.

@[simp]

theorem Cslib.Crypto.PRG.Generator.realExperiment_predictionTest {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : G.realExperiment (predictionTest i predictor) = G.predictionExperiment i predictor

The real experiment against the test built from a predictor is the prediction experiment.

@[simp]

theorem Cslib.Crypto.PRG.Generator.idealExperiment_predictionTest_apply_true {m : ℕ} (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : (idealExperiment (predictionTest i predictor)) true = 2⁻¹

On a uniform string, bit i is a uniform bit independent of the first i bits, so the test built from a predictor accepts with probability 1 / 2.

theorem Cslib.Crypto.PRG.Generator.advantage_predictionTest {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} (G : Generator Seed (Fin m → Bool)) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : G.advantage (predictionTest i predictor) = G.predictionAdvantage i predictor

The test built from a predictor has the advantage of the predictor.

theorem Cslib.Crypto.PRG.Generator.Secure.unpredictable {Seed : Type u_1} [Fintype Seed] [Nonempty Seed] {m : ℕ} {G : Generator Seed (Fin m → Bool)} {Admissible : Adversary (Fin m → Bool) → Prop} {AdmissiblePredictor : (i : Fin m) → Adversary (Fin ↑i → Bool) → Prop} {ε : NNReal} (hG : G.Secure Admissible ε) (hred : ∀ (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)), AdmissiblePredictor i predictor → Admissible (predictionTest i predictor)) : G.Unpredictable AdmissiblePredictor ε

Security implies unpredictability Boneh and Shoup, Theorem 3.4. If every admissible test has advantage at most ε, and the tests built from admissible predictors are admissible, then every admissible predictor has advantage at most ε.