Polynomially many semantic game hops

The concrete hybrid inequality adds the advantages of adjacent games. The asymptotic theorem requires a single negligible bound that works for every hop at each security parameter. Merely assuming negligibility separately for each fixed hop does not suffice when the number of hops grows with the parameter. The common bound may depend on the distinguisher.

The signed telescoping identities are stated over the reals, where subtraction is exact; the advantage bounds that follow from them are stated in the nonnegative reals.

Main results

• Game.advantage_hybrid_average: exact loss for a uniformly sampled, padded hybrid hop.
• Game.advantage_hybrid_le_sum: the endpoint advantage is bounded by adjacent advantages.
• Game.Indistinguishable.hybrid: polynomially many hops preserve indistinguishability.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 9.3.

theorem Cslib.Crypto.Game.succProbability_uniform {α : Type u_1} [Fintype α] [Nonempty α] (games : α → Game) : succProbability ((Probability.PMF.uniformOfFintype α).bind games) = (∑ a : α, (games a).succProbability) / ↑(Fintype.card α)

A uniformly selected experiment succeeds with the average of its success probabilities.

theorem Cslib.Crypto.Game.succProbability_hybrid_average (games : ℕ → Game) (hops capacity : ℕ) [NeZero capacity] (hle : hops ≤ capacity) : ↑(games 0).succProbability - ↑(games hops).succProbability = ↑capacity * (↑(succProbability ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then games ↑i else PMF.pure false)) - ↑(succProbability ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then games (↑i + 1) else PMF.pure false)))

Randomly choosing an adjacent hybrid telescopes signed gaps. Unused indices run the same rejecting game on both sides. This gives one reduction for every security parameter, with loss capacity, without selecting a parameter-dependent best hop.

theorem Cslib.Crypto.Game.advantage_hybrid_average (games : ℕ → Game) (hops capacity : ℕ) [NeZero capacity] (hle : hops ≤ capacity) : (games 0).advantage (games hops) = ↑capacity * advantage ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then games ↑i else PMF.pure false) ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then games (↑i + 1) else PMF.pure false)

Averaging adjacent hybrids also preserves distinguishing advantage, with the sampling-range loss and no parameter-dependent choice of the best hop.

theorem Cslib.Crypto.Game.succProbability_hybrid_reduction (games game1 game2 : ℕ → Game) (hops capacity : ℕ) [NeZero capacity] (hle : hops ≤ capacity) (loss : ℝ) (hstep : ∀ i < hops, ↑(games i).succProbability - ↑(games (i + 1)).succProbability = loss * (↑(game1 i).succProbability - ↑(game2 i).succProbability)) : ↑(games 0).succProbability - ↑(games hops).succProbability = ↑capacity * loss * (↑(succProbability ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then game1 ↑i else PMF.pure false)) - ↑(succProbability ((Probability.PMF.uniformOfFintype (Fin capacity)).bind fun (i : Fin capacity) => if ↑i < hops then game2 ↑i else PMF.pure false)))

Local reductions with a common signed loss combine into one uniformly selected reduction. The proof needs no choice of a best hop depending on the security parameter.

theorem Cslib.Crypto.Game.advantage_hybrid_le_sum (games : ℕ → Game) (hops : ℕ) : (games 0).advantage (games hops) ≤ ∑ i ∈ Finset.range hops, (games i).advantage (games (i + 1))

The advantage between the endpoints is at most the sum of all adjacent advantages.

theorem Cslib.Crypto.Game.advantage_hybrid_le (games : ℕ → Game) (hops : ℕ) (ε : NNReal) (hstep : ∀ i < hops, (games i).advantage (games (i + 1)) ≤ ε) : (games 0).advantage (games hops) ≤ ↑hops * ε

A common bound on each hop gives the usual linear loss in the number of hops.

theorem Cslib.Crypto.Game.negligible_hybrid {games : ℕ → ℕ → Game} {hops : ℕ → ℕ} {ε : ℕ → NNReal} (hpoly : PolynomiallyBounded hops) (hε : Negligible ε) (hstep : ∀ (n i : ℕ), i < hops n → (games n i).advantage (games n (i + 1)) ≤ ε n) : Negligible fun (n : ℕ) => (games n 0).advantage (games n (hops n))

Polynomially many hops with a common negligible bound have negligible total advantage.

theorem Cslib.Crypto.Game.Indistinguishable.hybrid {Adversary : Type u_1} {games : Adversary → ℕ → ℕ → Game} {Admissible : Adversary → Prop} {hops : ℕ → ℕ} (hpoly : PolynomiallyBounded hops) (hstep : ∀ (adversary : Adversary), Admissible adversary → ∃ (ε : ℕ → NNReal), Negligible ε ∧ ∀ (n i : ℕ), i < hops n → (games adversary n i).advantage (games adversary n (i + 1)) ≤ ε n) : Indistinguishable (fun (adversary : Adversary) (n : ℕ) => games adversary n 0) (fun (adversary : Adversary) (n : ℕ) => games adversary n (hops n)) Admissible

A hybrid argument with a common hop bound for each admissible adversary.