The rewinding lemma

A two-stage experiment runs a first stage with outcome s, draws a challenge t uniformly from a nonempty finite type T, and lets a second stage answer t from s; it succeeds when a test ok s t a of the answer a passes. Rewinding keeps s and reruns the second stage on a fresh independent challenge. Boneh and Shoup's rewinding lemma ([BS23], Lemma 19.2) says that if one run succeeds with probability ε and N is the number of challenges, then both runs succeed with distinct challenges with probability at least ε² − ε / N (sq_sub_le_twice). Consequently ε ≤ 1 / N + √δ for that probability δ (le_inv_add_sqrt_twice), the form that turns a bound on δ into one on ε.

The second stage may use fresh randomness in each run. This generalizes the book's deterministic f(X, Y): averaging over the second stage's coins turns the indicator into a success probability p(s, t) ∈ [0, 1], and the proof needs only p ^ 2 ≤ p. The first stage may have infinitely many outcomes. The statements are exact; no efficiency is involved.

The experiments are written in do notation for PMF, whose monad lives in a single universe; since they return a PMF Bool, the outcome, challenge and answer types are in Type.

Main definitions

• Cslib.Probability.Rewinding.once: one run of the two-stage experiment.
• Cslib.Probability.Rewinding.twice: two runs sharing the first stage, with independent challenges and second-stage randomness.

Main results

• Cslib.Probability.Rewinding.sq_sub_le_twice: ε² − ε / N ≤ δ ([BS23], Lemma 19.2).
• Cslib.Probability.Rewinding.le_inv_add_sqrt_twice: ε ≤ 1 / N + √δ.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Lemma 19.2 and the proof of Theorem 19.1.

noncomputable def Cslib.Probability.Rewinding.once {S T A : Type} [Fintype T] [Nonempty T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) : PMF Bool

One run of a two-stage experiment: the first stage, a uniform challenge t, the second stage's answer a to t, and the test ok s t a.

noncomputable def Cslib.Probability.Rewinding.twice {S T A : Type} [Fintype T] [Nonempty T] [DecidableEq T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) : PMF Bool

Rewinding: one first stage, then the second stage on two independent uniform challenges with independent randomness. It succeeds when both answers pass their tests and the challenges are distinct.

Proof of the rewinding lemma

The rewinding lemma

theorem Cslib.Probability.Rewinding.sq_sub_le_twice {S T A : Type} [Fintype T] [Nonempty T] [DecidableEq T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) : ((once first answer ok) true).toReal ^ 2 - ((once first answer ok) true).toReal / ↑(Fintype.card T) ≤ ((twice first answer ok) true).toReal

Rewinding lemma ([BS23], Lemma 19.2): if one run succeeds with probability ε, then two runs sharing the first stage succeed with distinct challenges with probability at least ε ^ 2 - ε / N, where N is the number of challenges.

theorem Cslib.Probability.Rewinding.le_inv_add_sqrt_twice {S T A : Type} [Fintype T] [Nonempty T] [DecidableEq T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) : ((once first answer ok) true).toReal ≤ 1 / ↑(Fintype.card T) + √((twice first answer ok) true).toReal

The rewinding lemma solved for the one-run probability ([BS23], from the proof of Theorem 19.1): ε ≤ 1 / N + √δ.