Fundamental Lemma of Game Playing + Multi-Query Games #
This file provides three layers of game-playing infrastructure:
Shoup's Fundamental Lemma (bad-event lemma): if two games are identical until a "bad" event occurs, then their distinguishing advantage is bounded by the probability of the bad event.
Multi-query game abstraction: a generic framework for games where an adversary makes
qadaptive oracle queries, with a boundAdv_q <= q * Adv_1via the hybrid argument.Lazy/eager sampling equivalence: the two standard sampling strategies for random oracles produce the same distribution.
Main Results #
Fundamental Lemma #
IdenticalUntilBad-- games agree unless bad occursadvantage_upto_bad-- Advantage(G0, G1) <= Pr[bad] (Shoup 2004, Lemma 1)advantage_upto_bad_A-- adversary-parameterized versionUpToBad-- bundled: identical-until-bad + bad probability bounduptobad_advantage-- extract advantage bound from UpToBad
Multi-Query Games #
MultiQueryGame-- init/query/finalize structureMultiQueryGame.run-- execute with q queriesMultiQueryGame.single_to_multi_bound-- Adv_q <= q * Adv_1
Lazy/Eager Sampling #
lazy_sample-- sample on first query, cache for latereager_sample-- sample all values upfrontlazy_eager_equiv-- they produce the same distribution
Cross-Validation #
| Property | This file | Reference |
|---|---|---|
| Bad-event bound | advantage_upto_bad | Shoup 2004, Lemma 1 |
| Identical-until-bad | IdenticalUntilBad | Bellare-Rogaway 2006, Def. 1 |
| Multi-query hybrid | single_to_multi_bound | Boneh-Shoup, Thm 4.4 |
| Lazy/eager equiv | lazy_eager_equiv | Bellare-Rogaway 2006, Lemma 1 |
Equivalent formalizations:
- EasyCrypt:
upto_badtactic /Uptotheory - CryptoVerif:
find_coll/eventdeclarations - SSProve (Rocq):
rules_RHS/ package composition
References #
- Shoup, Sequences of Games: A Tool for Taming Complexity in Security Proofs, ePrint 2004/332, Lemma 1.
- Bellare & Rogaway, The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs, EUROCRYPT 2006.
- Boneh & Shoup, A Graduate Course in Applied Cryptography, Ch. 4.
Identical-Until-Bad #
Two computations are "identical until bad" if they produce the same output distribution conditioned on a bad event not occurring.
This is the core semantic predicate behind Shoup's fundamental lemma and the Bellare-Rogaway code-based game-playing framework.
Two Bool games are identical until bad if:
- When
baddoes NOT happen, they produce the same output - The probability of
badis bounded
Formally: G₀ and G₁ are coupled such that they agree
whenever a predicate ¬bad holds on the shared randomness.
The inequality G₀(b, h') ≤ G₁(b, h') + bad(true, h') captures
that any excess probability mass in G₀ relative to G₁ is accounted
for by the bad event. When bad doesn't fire (bad probability = 0),
the two games produce identical distributions.
- agree_unless_bad (h : Core.Heap) (b : Bool) (h' : Core.Heap) : (G₀ h) (some (b, h')) ≤ (G₁ h) (some (b, h')) + (bad h) (some (true, h'))
When bad doesn't happen, the games agree
Instances For
Fundamental Lemma (Statement) #
The full proof of Shoup's lemma requires a coupling argument over the joint distribution of (game output, bad event). We state the key result as an axiom and provide the proof sketch.
Proof sketch (Shoup, Lemma 1): Define events S₀, S₁ (game outputs 1) and F (bad event). Then: |Pr[S₀] - Pr[S₁]| = |Pr[S₀ ∧ ¬F] + Pr[S₀ ∧ F] - Pr[S₁ ∧ ¬F] - Pr[S₁ ∧ F]| = |Pr[S₀ ∧ F] - Pr[S₁ ∧ F]| (since S₀∧¬F = S₁∧¬F) ≤ Pr[F] (since Pr[Sᵢ ∧ F] ≤ Pr[F])
EasyCrypt proves this via the upto_bad tactic.
Shoup's Fundamental Lemma: if two games are identical until bad, then their advantage is bounded by the probability of the bad event.
Requires both G₀ and G₁ to be NoFail: without this, the
IdenticalUntilBad inequality (one-directional, applied to b = true)
only gives prTrue G₀ ≤ prTrue G₁ + prTrue bad. The reverse direction
needs the b = false case combined with prTrue + prFalse = 1,
which requires NoFail.
Bad-event lemma with adversary: if two computations are identical until bad for all adversaries, the adversary-parameterized advantage is bounded by the bad-event probability.
Hypotheses: NoFail on G₀, G₁, and (per-input) on the adversary A.
These combine via SPComp.bind_noFail to give NoFail on the composed
games, which advantage_upto_bad requires.
Proof strategy: For any adversary A, instantiate advantage_upto_bad
on the composed games G₀.bind A and G₁.bind A.
UpToBad: Bundled Bad-Event Technique #
In practice, a game-hopping step via the bad-event technique requires:
- A proof that the two games are identical until bad
- A bound on the probability of the bad event
The UpToBad structure bundles both, making it easy to extract
the advantage bound in one step.
Bundled "up to bad" technique: games are identical until bad,
and the bad-event probability is bounded by ε_bad. Both games
must be NoFail (required by advantage_upto_bad).
- identical : IdenticalUntilBad G₀ G₁ bad
The games are identical unless bad occurs
- noFail_left : SPComp.NoFail G₀
G₀ never fails
- noFail_right : SPComp.NoFail G₁
G₁ never fails
The bad event probability is bounded
Instances For
Extract the advantage bound from an UpToBad witness.
Bundled UpToBad with adversary: for adversary-parameterized games.
- identical (A : α → Core.SPComp Bool) : IdenticalUntilBad (G₀.bind A) (G₁.bind A) bad
The games are identical until bad for all adversaries
- noFail_left : SPComp.NoFail G₀
G₀ never fails
- noFail_right : SPComp.NoFail G₁
G₁ never fails
The bad event probability is bounded
Instances For
Extract the advantage bound from an UpToBadA witness, given a
NoFail-preserving adversary.
Corollary: Union Bound for Multiple Bad Events #
When a proof involves multiple bad events, the union bound gives:
Pr[bad₁ ∨ bad₂ ∨ ... ∨ bad_n] ≤ Pr[bad₁] + ... + Pr[bad_n]
This composes with the fundamental lemma to give multi-hop bounds.
Union bound for two bad events under IsPure+NoFail: the probability of either bad event firing is at most the sum of their individual probabilities.
Hypotheses: Both bad₁ and bad₂ must be IsPure+NoFail. The
bound is false without heap-purity on bad₂ — counter-example:
bad₁ writes the heap and returns false, bad₂ reads the heap and
returns whether it was written; then chained prTrue = 1 but
prTrue bad₁ Heap.empty + prTrue bad₂ Heap.empty = 0.
Proof: Decompose prTrue(bind bad₁ k) via prTrue_isPure_noFail_bind
(NomPkgBridge). The first branch (b₁=true) makes the inner expression
true || _ = true so the prTrue equals bad₂'s mass = 1 (NoFail). The
second branch (b₁=false) reduces to pure b₂, so the prTrue equals
prTrue bad₂. Bound: d₁(true)·1 + d₁(false)·prTrue bad₂ ≤ d₁(true) + prTrue bad₂ since d₁(false) ≤ 1.
Union bound for a finite list of bad events.
Equations
- CatCrypt.Crypto.BadEvent.bad_union [] = CatCrypt.Core.SPComp.pure false
- CatCrypt.Crypto.BadEvent.bad_union [b] = b
- CatCrypt.Crypto.BadEvent.bad_union (b :: bs) = do let b₁ ← b let b₂ ← CatCrypt.Crypto.BadEvent.bad_union bs CatCrypt.Core.SPComp.pure (b₁ || b₂)
Instances For
Chaining: Bad Event + Hybrid Argument #
Combining the fundamental lemma with the hybrid argument gives a powerful pattern: each hybrid step is an "identical until bad" transition, and the total advantage sums the bad-event probabilities.
Bad-event hybrid bound: if each of n hybrid steps is identical
until bad with bad-event probability at most ε, then the total
advantage is at most n * ε.
This is the standard pattern for multi-step game-hopping proofs where each step introduces a collision or failure event.
Multi-Query Game Abstraction #
A generic multi-query game models the common pattern in cryptographic security definitions (IND-CPA, PRF, MAC, etc.) where an adversary interacts with an oracle over multiple rounds:
- Initialize internal state
- Query the oracle
qtimes, updating state each time - Finalize by producing a Boolean decision
The key theorem single_to_multi_bound formalizes the standard
reduction: if distinguishing a single query costs advantage ε₁,
then distinguishing q queries costs at most q * ε₁.
A multi-query game parameterized by state, input, and output types.
This captures the structure of IND-CPA, PRF, MAC, and other multi-query security definitions. The adversary's strategy is encoded by the sequence of inputs; the game handles the internal oracle computation.
In the PRF setting:
State= key (or ⊥ for ideal)Input= domain elementOutput= range elementinit= key generation (or table init)query= evaluate PRF (or sample random)finalize= adversary's decision
- init : Core.SPComp State
Initialize the game state (e.g., key generation)
- query : State → Input → Core.SPComp (State × Output)
Process one oracle query: takes current state and query input, returns updated state and query output
- finalize : State → Core.SPComp Bool
Produce the final decision from the accumulated state
Instances For
Execute a multi-query game with a given sequence of inputs.
Processes q queries sequentially, threading state through each
query, then finalizes. The result is a SPComp Bool suitable
for computing advantage.
The recursion unfolds as:
s₀ ← init
(s₁, o₁) ← query s₀ (inputs 0)
(s₂, o₂) ← query s₁ (inputs 1)
...
(s_q, o_q) ← query s_{q-1} (inputs (q-1))
finalize s_q
Equations
Instances For
Helper: run q queries starting from state s, using inputs at
indices 0, 1, ..., q-1.
Equations
- One or more equations did not get rendered due to their size.
- CatCrypt.Crypto.BadEvent.MultiQueryGame.run.runQueries qry s inputs 0 = CatCrypt.Core.SPComp.pure s
Instances For
An alternative, more explicit execution that collects all outputs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Run queries with the first switch using qry_ideal and the rest
using qry_real. Helper for hybrid game construction.
Equations
- One or more equations did not get rendered due to their size.
- CatCrypt.Crypto.BadEvent.MultiQueryGame.hybridQueries qry_ideal qry_real s inputs switch 0 = CatCrypt.Core.SPComp.pure s
Instances For
The i-th hybrid game between G_real and G_ideal: first i
queries use the ideal oracle, remaining queries use the real oracle.
This is the standard hybrid construction for multi-query reductions:
hybrid 0= all-real gamehybrid q= all-ideal gamehybrid iandhybrid (i+1)differ in exactly one query
Assumes G_real and G_ideal share the same init and finalize
(they differ only in the oracle).
Equations
Instances For
Single-to-multi-query reduction: if distinguishing a single
query between G_real and G_ideal costs advantage at most ε₁,
then distinguishing q queries costs at most q * ε₁.
This formalizes the standard textbook reduction (Boneh-Shoup Thm 4.4): the hybrid argument interpolates between all-real and all-ideal, and each step reduces to the single-query distinguishing problem.
Proof strategy: Construct q+1 hybrid games where hybrid i
uses the ideal oracle for the first i queries and the real oracle
for the rest. Each adjacent pair of hybrids differs in exactly one
query, so the per-step advantage is at most ε₁. Apply
advantage_hybrid_uniform to sum the q steps.
Lazy/Eager Sampling Equivalence #
A fundamental technique in game-playing proofs: a random oracle can be implemented either by:
- Lazy sampling: sample a random value the first time a query is made, then return the cached value on subsequent queries
- Eager sampling: sample the entire random function upfront, then look up values deterministically
These two strategies produce identical distributions. This equivalence is used pervasively in PRF, ROM, and ideal cipher proofs.
Reference: Bellare & Rogaway 2006, Lemma 1.
Lazy sampling oracle: maintains a partial function table : D → Option R.
On query x:
- If
table x = some r, returnr(cached) - If
table x = none, sampler ← uniform R, update table, returnr
This is the standard "program-on-the-fly" implementation of a random oracle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Eager sampling oracle: given a total function f : D → R (sampled upfront),
simply look up the value. No state update needed since everything is
precomputed.
The function f is typically obtained by sampling from the uniform
distribution over D → R (or equivalently, sampling each f(d)
independently).
Equations
Instances For
Process a list of queries via lazy sampling, threading the table. Each query either returns a cached result or samples fresh.
Equations
- One or more equations did not get rendered due to their size.
- CatCrypt.Crypto.BadEvent.lazy_process [] table = CatCrypt.Core.SPComp.pure []
Instances For
Process a list of queries via eager sampling: sample the full function upfront, then look up each query deterministically.
Equations
- CatCrypt.Crypto.BadEvent.eager_process queries = do let f ← CatCrypt.Core.SPComp.sample (D → R) CatCrypt.Core.SPComp.pure (List.map f queries)
Instances For
Helpers for lazy_eager_equiv #
These reduce both lazy and eager sampling to a common sequential_sample
intermediate (iid R-uniforms). The lazy half is a straightforward induction;
the eager half uses Equiv.piSplitAt + SDistr.uniform_bind_equiv_comp to
factor uniform (D → R) into uniform R × uniform ({d // d ≠ x} → R),
recursing over the queries.
Sequential iid uniform sampling — n fresh uniforms on R, paired into a list.
Equations
Instances For
Lazy/eager sampling equivalence: for any sequence of distinct queries, the lazy and eager sampling strategies produce the same joint distribution over outputs.
Composes lazy_process_eq_sequential (proven) and
eager_process_eq_sequential (deferred, see its docstring) via the
common sequential_sample intermediate.
This is Bellare-Rogaway 2006, Lemma 1 (also implicit in Shoup 2004).
Single-query lazy/eager equivalence: for a single query x on
an empty table, lazy sampling and uniform sampling produce the same
distribution.
This is the base case of the full lazy/eager equivalence.
Composition: Bad Event + Lazy/Eager #
A common proof pattern combines the bad-event lemma with lazy/eager equivalence:
- Replace eager sampling with lazy sampling (zero cost, by
lazy_eager_equiv) - Introduce a bad event (collision, etc.)
- Bound the game transition by the bad-event probability
This pattern appears in PRF, MAC, and signature security proofs.
Lazy-to-eager via bad event: if a game using lazy sampling is identical-until-bad to a game using eager sampling (where bad = collision), then the advantage is bounded by the collision probability.
This combines lazy_eager_equiv with advantage_upto_bad. NoFail
hypotheses are required by the (now-proven) advantage_upto_bad.