Cryptobox Game-Hopping Chain #
This file proves the game-hopping decomposition for the Cryptobox security proof,
replacing the monolithic hdecomp hypothesis with a transparent chain of game hops.
Game-hopping chain #
The proof proceeds through intermediate games:
G₀ = PKAE(real)
≈ G₁ = PKAE_cc(real) -- PKEY switching (FEL)
≈ G₂ = PKAE_cc(ideal) -- NIKE + AE combined switch
≈ G₃ = PKAE(ideal) -- PKEY unswitching (FEL)
where PKAE_cc uses collision-checking in the GEN oracle.
Main results #
PKAE_eq_PKEY_nocheck- PKAE = PKEY(no-check) with reduction adversary (by rfl)PKAE_cc_eq_PKEY_check- PKAE_cc = PKEY(check) with reduction adversary (by rfl)pkae_pkey_step- PKEY switching step equalspkeyAdvantageof reductionpkae_game_hopping- Full three-step decomposition via triangle inequalitycryptobox_security_chain- Main theorem with explicit game-hopping structurecryptobox_security_full- Full 4-component security bound
Architecture #
The PKEY switching steps (G₀ ↔ G₁ and G₂ ↔ G₃) are proved by showing that PKAE and PKAE_cc are instances of the PKEY game with a reduction adversary. These are definitional equalities — the reduction is the identity on oracle structure, just routing enc/dec through the PKEY oracles.
The middle step (G₁ → G₂) combines NIKE switching and AE switching. This is further decomposed into:
- NIKE switching: replace real shared keys with random keys for honest-honest pairs
- KEY structural: KEY(0) = KEY(1) when inputs are already random
- AE switching: replace real encryption with ideal encryption (hybrid argument)
References #
- Dupressoir et al., "How Hard Can It Be?" (ASIACRYPT 2025)
- Dupressoir et al., "Bringing SSP to EasyCrypt" (CSF 2022)
- Myssenburg et al., Rocq SSProve Cryptobox
PKAE with Collision-Checking GEN #
PKAE game with collision-checking GEN oracle.
Identical to PKAE except genOracle N true is used instead of
genOracle N false. This enables the FEL argument: PKAE and PKAE_cc
agree unless a public key collision occurs during key generation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PKEY Reduction Adversary #
Reduction from PKAE to PKEY: wraps a PKAE adversary into a PKEY adversary.
Given PKEY oracles (for key management), constructs the PKAE oracle interface by routing encryption/decryption through the given PKEY oracles.
The parameter b controls whether encryption/decryption is real (false)
or ideal (true).
Key property: PKEY N bGen (R_PKEY N E I bEnc A) equals:
PKAE N E I bEnc AwhenbGen = false(no collision check)PKAE_cc N E I bEnc AwhenbGen = true(collision check)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reduction Correctness #
These show that PKAE and PKAE_cc are instances of the PKEY game with the reduction adversary. The proofs are by definitional equality.
PKAE = PKEY(no-check) with PKEY reduction adversary.
This is the fundamental structural fact: PKAE N E I b A is exactly
the PKEY game with no collision checking, where the adversary is
R_PKEY N E I b A.
PKAE_cc = PKEY(collision-check) with PKEY reduction adversary.
PKEY Switching Steps #
Advantage is symmetric: Advantage G₀ G₁ = Advantage G₁ G₀.
The distance between PKAE and PKAE_cc equals the PKEY advantage of the reduction adversary.
This is the key reduction: the PKEY switching step in the game-hopping chain is exactly the PKEY advantage for the appropriate adversary.
The distance from PKAE_cc to PKAE is also the PKEY advantage (by symmetry).
Game-Hopping Chain #
Game-hopping decomposition for PKAE.
The PKAE advantage decomposes into three steps via triangle inequality:
PKEY switching (real side):
PKAE(real) → PKAE_cc(real)Advantage =pkeyAdvantage N (R_PKEY false A)(collision bound)Middle step (NIKE + AE):
PKAE_cc(real) → PKAE_cc(ideal)Advantage captures both NIKE switching and AE switchingPKEY switching (ideal side):
PKAE_cc(ideal) → PKAE(ideal)Advantage =pkeyAdvantage N (R_PKEY true A)(collision bound)
The PKEY steps are proved reductions. The middle step is the "hard" part requiring NIKE and AE security arguments.
Main Security Theorem (Chain Version) #
Cryptobox security theorem (game-hopping chain version).
The PKAE advantage is bounded by 2 * pkey_eps + middle_eps, where:
pkey_epsbounds the PKEY advantage for both reduction adversariesmiddle_epsbounds the NIKE + AE combined switching step
Compared to cryptobox_security, this version:
- Proves the PKEY reductions (not hypothesized)
- Makes the game-hopping structure explicit
- Isolates the remaining proof obligations (PKEY FEL, NIKE+AE)
Middle Step Decomposition #
The middle step Advantage (PKAE_cc false) (PKAE_cc true) captures the
combined NIKE switching and AE switching. It can be further decomposed
into NIKE and AE contributions.
Conceptual decomposition #
PKAE_cc(real)
≈ PKAE_nikeSwitch -- NIKE: real → random shared keys
= PKAE_nikeSwitch -- KEY structural: random input → KEY(0)=KEY(1)
≈ PKAE_cc(ideal) -- AE: real → ideal encryption
NIKE switching #
In PKAE_cc(real), the enc/dec oracles compute shared keys via N.sharedkey.
After NIKE switching, honest-honest pairs use uniformly random shared keys
instead. This requires:
- Storing sampled shared keys per session (using
nikeKeysLoc) - The NIKE advantage bounds the distinguishing probability
AE switching (hybrid argument) #
After NIKE switching, shared keys for honest-honest sessions are random. The AE step switches from real encryption to ideal (log-based) encryption. This is decomposed via a hybrid argument over sessions:
- Each session contributes at most
sae_eps(i)distinguishing probability - Total AE advantage ≤
Σ sae_eps(i)
The middle step advantage: distance between collision-checking PKAE with real vs ideal enc/dec.
Equations
Instances For
NIKE-Switched Intermediate Game #
Get or sample a random shared key for a session.
Looks up the shared key cache (nikeKeysLoc); if found, returns the
cached key. Otherwise, samples a fresh random key, stores it, and
returns it. This ensures each session gets a consistent random key
across multiple enc/dec calls.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PKAE with collision-checking GEN and NIKE-switched shared keys.
For honest-honest pairs: shared keys are sampled uniformly at random
(cached per session via nikeKeysLoc), then used with real encryption
(E.enc, E.dec).
For corrupt pairs: shared keys are computed via N.sharedkey (real),
then used with real encryption.
This is the intermediate game between:
The NIKE switching step (PKAE_cc false → PKAE_nikeSwitch) replaces
real shared keys with random keys for honest-honest pairs.
The AE switching step (PKAE_nikeSwitch → PKAE_cc true) replaces
real encryption with ideal encryption for honest sessions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The middle step decomposes into NIKE switching + AE switching via the NIKE-switched intermediate game.
The NIKE switching advantage: distance between real shared keys and random shared keys for honest-honest pairs.
Equations
Instances For
The AE switching advantage: distance between real encryption and ideal encryption when shared keys are already random.
Equations
Instances For
Middle step bounded by NIKE + AE step advantages.
Full Decomposition #
Combining the game-hopping chain with the middle step decomposition gives the full security bound.
Full Cryptobox security bound with explicit game-hopping structure.
Decomposes PKAE advantage into:
2 * pkey_eps: Two PKEY switching steps (collision bounds)nike_eps: NIKE switching (shared key indistinguishability)ae_eps: AE switching (encryption indistinguishability)
This is the most structured version of the Cryptobox security theorem. Each hypothesis corresponds to a single, well-defined proof obligation:
h_pkey_real/ideal: Bound PKEY collision probability (FEL)h_nike: Bound NIKE advantage (DDH or similar assumption)h_ae: Bound AE advantage (hybrid argument over sessions)
Corollaries #
Specializations of the full security theorem for common scenarios.
When the PKEY collision bound is zero (e.g., infinite key space), the PKAE advantage reduces to just NIKE + AE advantages.
When NIKE and AE are perfectly secure (e.g., information-theoretic), the PKAE advantage is bounded purely by the collision probability.
Proof Obligation Summary #
The cryptobox_security_full theorem reduces the PKAE security proof to
four independent proof obligations. Here we document what each requires:
1. PKEY collision bound (h_pkey_real, h_pkey_ideal) #
Statement: pkeyAdvantage N (R_PKEY N E I b A) ≤ pkey_eps
Proof approach: FEL (Failure Event Lemma)
- Define bad event: a GEN call produces a pk that matches an existing honest/corrupt key
- Show
PKEY N false (R_PKEY b A)andPKEY N true (R_PKEY b A)agree when no collision - Bound collision probability: ≤
q_gen * q_csetpk / |PK|(birthday-type bound) - Apply
advantage_le_prBadfromFailureEvent.lean
Required infrastructure: Oracle composition reasoning (shared prefix argument)
Status: Reduction proven (R_PKEY), FEL structure documented (PKEY.lean), concrete probability bound requires oracle-level analysis.
2. NIKE switching (h_nike) #
Statement: nikeStepAdvantage N E I A ≤ nike_eps
Proof approach: Reduction to NIKE game
- Construct adversary
R_NIKEthat uses NIKE sharedkey oracle for key computation - Show
PKAE_cc false A≈GNIKE N false pkeyO (R_NIKE A)(structural equivalence) - Show
PKAE_nikeSwitch A≈GNIKE N true pkeyO (R_NIKE A)(structural equivalence) - Conclude:
nikeStepAdvantage ≤ nikeAdvantage N pkeyO (R_NIKE A)
Required infrastructure: Shared key caching equivalence (real keys are deterministic, so caching doesn't change behavior; random keys need consistency).
Status: PKAE_nikeSwitch defined with explicit caching mechanism. Reduction requires structural equivalence between inline and cached key computation.
3. AE switching (h_ae) #
Statement: aeStepAdvantage N E I A ≤ ae_eps
Proof approach: Hybrid argument over sessions
- Define hybrid game
H(i): firstihonest sessions use ideal encryption, remaining use real encryption - Show
H(0)= PKAE_nikeSwitch,H(q)= PKAE_cc true (up to KEY structural equiv) - Bound per-step:
Advantage H(i) H(i+1) ≤ saeAdvantage i - Apply triangle inequality:
ae_eps = Σ saeAdvantage(i)
Required infrastructure: Per-session oracle isolation, AE→SAE reduction.
Status: ae_hybrid_bound proven in Cryptobox.lean (triangle + sum_le_sum). Per-session SAE reduction defined (R_GSAE). Structural equivalences needed.
NIKE Reduction Architecture #
The NIKE switching step (PKAE_cc false → PKAE_nikeSwitch) is proven via
reduction to the NIKE game:
PKAE_cc false ≈ GNIKE N false pkeyO (R_NIKE A) ≈? GNIKE N true pkeyO (R_NIKE A) ≈ PKAE_nikeSwitch
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This gap is the caching equivalence
The caching equivalence states that GNIKE N false (which caches deterministic
shared keys) produces the same adversary-observable behavior as inline computation
(which doesn't cache). This follows from:
N.sharedkeyis a pure function → cache always contains the correct value- The extra heap writes to
nikeKeysLoc/nikeHonestLocdon't affect any oracle the adversary can query (PKEY oracles readpkHonestLoc/skStoreLoc/pkCorruptLoc, not NIKE locations)
Formally proving this requires "heap frame" reasoning showing that oracle behavior is independent of locations they don't read. This is left as future work.
NIKE Reduction Adversary #
Adapted NIKE reduction that properly threads PKEY oracles.
Given PKEY oracles and a NIKE oracle, constructs a PKAE oracle interface. The enc/dec oracles check honesty:
- If both parties are honest: query the NIKE oracle for the shared key
- If either is corrupt: compute shared key directly via
N.sharedkey
This matches the structure of PKAE_cc/PKAE_nikeSwitch, where
the honest-honest case uses a potentially different key source.
Compare with R_GNIKE in Cryptobox.lean, which routes ALL pairs
through the NIKE oracle (no honesty check). This adapted version
is needed because the NIKE game only provides different behavior
for honest-honest pairs; corrupt pairs always use N.sharedkey.
Equations
- One or more equations did not get rendered due to their size.
Instances For
GNIKE Instantiation with R_NIKE #
GNIKE N b pkeyO (R_NIKE N E I A pkeyO) unfolds to R_NIKE applied to
the sharedkeyOracle N b pkeyO — this is definitional.
This confirms that the NIKE game with the reduction adversary correctly
threads the PKEY oracles and the shared key oracle through the PKAE
oracle interface constructed by R_NIKE.
The NIKE advantage of the reduction adversary R_NIKE measures
the adversary's ability to distinguish real from random shared keys
when routed through the PKAE oracle interface.
This is the "right-hand side" of the NIKE reduction:
nikeStepAdvantage N E I A ≤ nikeAdvantage N pkeyO (R_NIKE N E I A)
modulo the caching equivalence gap.
Equations
- CatCrypt.Examples.Cryptobox.nikeReductionAdvantage N E I A pkeyO = CatCrypt.Examples.Cryptobox.nikeAdvantage N pkeyO (CatCrypt.Examples.Cryptobox.R_NIKE N E I A)
Instances For
Deterministic Caching Lemma #
A general principle: if a function f is deterministic (pure),
then caching its result doesn't change the return value.
Specifically, for a map cache : K → Option V and a function f : K → V:
- Cache miss: compute
f(k), store in cache, returnf(k) - Cache hit: return
cache[k]
If cache[k] = some (f k) for all cached entries (invariant),
then both paths return f(k).
This is the key reasoning principle for the NIKE caching equivalence:
N.sharedkey is deterministic, so the sharedkeyOracle N false
(which caches the result of N.sharedkey) returns the same value
as inline computation of N.sharedkey.
Variant with Option.getD: looking up k in a cache that satisfies
the invariant and defaulting to f k always yields f k.
NIKE Reduction Structure #
The NIKE switching step is bounded by the NIKE reduction advantage plus a
caching gap, obtained by inserting the two reduction games
GNIKE N false pkeyO (R_NIKE …) and GNIKE N true pkeyO (R_NIKE …) into the
chain and applying the triangle inequality twice:
PKAE_cc false → GNIKE N false (R_NIKE) → GNIKE N true (R_NIKE) → PKAE_nikeSwitch
The middle term is nikeReductionAdvantage. The two boundary terms are the
caching gap: the distance between inline shared-key computation
(PKAE_cc false, PKAE_nikeSwitch) and the cached computation with extra
heap writes to nikeKeysLoc/nikeHonestLoc performed by
sharedkeyOracle. Each boundary term is zero exactly when the extra heap
writes are invisible to the adversary's PKEY oracle queries — for the ideal
side (GNIKE N true) both games sample and cache random keys identically.
The NIKE step advantage is bounded by the NIKE reduction advantage plus a "caching gap" term that accounts for the difference between inline computation and cached computation with extra heap writes.
In the ideal case (GNIKE N true), the caching gap is zero because
both PKAE_nikeSwitch and GNIKE N true via R_NIKE sample random
keys and cache them in nikeKeysLoc.
In the real case (GNIKE N false), the caching gap captures the difference between:
PKAE_cc false: computesN.sharedkey pk_r sk_sinline (no cache)GNIKE N falseviaR_NIKE: computesN.sharedkey pk_r sk_s, caches innikeKeysLoc, also writesnikeHonestLoc
Since N.sharedkey is deterministic, the return values are identical;
only the heap state differs. The caching gap is therefore bounded by
the probability that the extra heap writes become observable.
When the caching gap is zero, the NIKE step advantage equals the NIKE reduction advantage. This is the expected case because:
N.sharedkeyis deterministic → caching doesn't change return values- Extra heap writes to
nikeKeysLoc/nikeHonestLocare invisible to the adversary's PKEY oracle queries
The hypothesis h_cache_zero formalizes "the caching gap is zero",
meaning the NIKE game with R_NIKE exactly equals the direct games.
Full Security with NIKE Reduction #
Combining cryptobox_security_full with the NIKE reduction gives a
version where the NIKE bound comes from a concrete reduction adversary.
Cryptobox security with explicit NIKE reduction.
This combines the full game-hopping decomposition with the NIKE reduction
adversary, making explicit that the NIKE step advantage is bounded by
the NIKE advantage of the reduction R_NIKE.
Compared to cryptobox_security_full, this version:
- Names the NIKE reduction adversary explicitly
- Connects the abstract
nike_epsto the concretenikeAdvantage - Includes the caching gap hypothesis that bridges the structural difference
Simplified version when the caching gap is zero.
When N.sharedkey is deterministic and extra heap writes are provably
invisible (the expected case), the caching gap vanishes and we get the
clean four-component bound.