PKEY: Public Key Management Game #

The PKEY game switching argument is a failure event lemma (FEL) application. The key insight is that genOracle N false and genOracle N true differ only in the collision check: when honest pk || corrupt pk = false (no collision), both branches execute identically. When a collision DOES occur, the b=true version fails (produces 0 mass) while the b=false version continues.

Proof Structure #

To prove pkeyAdvantage N A ≤ ε via FEL, one needs:

Up-to-bad agreement: PKEY N false A and PKEY N true A agree on outcomes where no collision occurred during execution. This follows from the observation that genOracle N false and genOracle N true diverge only at the collision check, and all other oracles (csetpk, getsk, honpk) are identical.
Bad probability bound: The probability that a collision occurs during PKEY N false A is at most ε. With q_gen GEN queries and q_csetpk CSETPK queries, each GEN call samples a pk uniformly, and the collision probability is at most (#honest + #corrupt) / |PK| per call. By union bound: Pr[collision] ≤ q_gen * q_csetpk / |PK|.

Comparison with Other Formalizations #

EasyCrypt (~200 lines): Proved via fel tactic with automatic oracle decomposition
Rocq SSProve (~150 lines): ADMITTED (structural equivalence axiom)
Our approach: The reduction PKAE → PKEY is proven (see GameHopping.lean); the FEL bound itself requires oracle composition reasoning not yet available

source

def CatCrypt.Examples.Cryptobox.pkeyCollision [CT : CryptoTypes] (h : Core.Heap) (pk : CryptoTypes.PK) :

Prop

Collision bad event for a single GEN call.

A collision occurs when the newly generated pk matches an existing honest or corrupt key. This is checked on the heap state BEFORE the honest flag is updated.

Equations

CatCrypt.Examples.Cryptobox.pkeyCollision h pk = (h.get CatCrypt.Examples.Cryptobox.pkHonestLoc pk = true ∨ h.get CatCrypt.Examples.Cryptobox.pkCorruptLoc pk = true)

Instances For

source

def CatCrypt.Examples.Cryptobox.pkeyBadFinal [CT : CryptoTypes] (h : Core.Heap) :

Prop

Collision predicate on final heap.

The "bad event" for the FEL: there exists a pk that is registered as BOTH honest and corrupt. This is a necessary consequence of any collision during execution (since GEN sets honest and CSETPK sets corrupt, a collision means some pk ends up with both flags set).

Note: this is a necessary but not sufficient condition for a collision during execution. A stronger formulation would track the collision flag explicitly (requiring an instrumented game).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.pkeyOracles_cc [CT : CryptoTypes] (N : NIKEScheme) :

PKEYOracles

PKEY collision-checking oracle record. Convenience for building oracle records.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.pkeyOracles_nocc [CT : CryptoTypes] (N : NIKEScheme) :

PKEYOracles

PKEY non-collision-checking oracle record.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CatCrypt.Examples.Cryptobox.PKEY_eq_with_oracles [CT : CryptoTypes] (N : NIKEScheme) (b : Bool) (A : PKEYOracles → Core.SPComp Bool) :

PKEY N b A = A (if b = true then pkeyOracles_cc N else pkeyOracles_nocc N)

PKEY game with explicit oracle record is definitionally equal to PKEY.

genOracle Analysis #

Properties of the collision check in genOracle. These are building blocks for proving the up-to-bad agreement condition.

source

theorem CatCrypt.Examples.Cryptobox.genOracle_unfold [CT : CryptoTypes] (N : NIKEScheme) (b : Bool) :

genOracle N b = do let pair ← N.pkgen have pk : CryptoTypes.PK := pair.1 have sk : CryptoTypes.SK := pair.2 let honest ← Core.SPComp.get pkHonestLoc let corrupt ← Core.SPComp.get pkCorruptLoc have __do_jp : Unit → Core.SPComp CryptoTypes.PK := fun (__r : Unit) => do let skMap ← Core.SPComp.get skStoreLoc Core.SPComp.set pkHonestLoc (Function.update honest pk true) Core.SPComp.set skStoreLoc (Function.update skMap pk sk) Core.SPComp.pure pk if b = true then if (honest pk || corrupt pk) = true then do let __r ← Core.SPComp.fail __do_jp __r else do let __r ← Core.SPComp.pure () __do_jp __r else do let __r ← Core.SPComp.pure () __do_jp __r

genOracle N false and genOracle N true differ only in the collision check.

When b = false: the collision check is skipped (SPComp.pure ()) When b = true: the collision check may fail (if coll then fail else pure ())

The rest of the oracle body (sample, read honest/corrupt/skMap, update, return pk) is identical in both cases.

PKEY FEL Application #

Application of the Failure Event Lemma to bound the PKEY advantage. The bad event is pkeyBadFinal: some public key is both honest and corrupt in the final heap.

source

theorem CatCrypt.Examples.Cryptobox.pkeyAdvantage_le_collision [CT : CryptoTypes] (N : NIKEScheme) (B : PKEYOracles → Core.SPComp Bool) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬pkeyBadFinal h' → (PKEY N false B Core.Heap.empty) (some (b, h')) = (PKEY N true B Core.Heap.empty) (some (b, h'))) (hll : Unary.isLossless (PKEY N false B)) :

pkeyAdvantage N B ≤ Unary.prEventComp (PKEY N false B) Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => pkeyBadFinal h'

PKEY advantage bounded by collision probability via FEL.

This instantiates advantage_le_prBad from FailureEvent.lean with the PKEY-specific bad event (pkeyBadFinal).

The two hypotheses that must be discharged for a specific adversary B:

Up-to-bad agreement (h_agree): When no collision occurs (no pk is both honest and corrupt in the final heap), the two PKEY games produce the same distribution. This follows from the fact that genOracle N false and genOracle N true differ only in the collision check, which is vacuous when no collision occurs.
For a concrete adversary, this requires showing that the adversary's oracle calls compose correctly — see agree_bind_left and agree_bind_both from FailureEvent.lean for the composition lemmas.
Losslessness (hll): The PKEY N false B game is lossless (total mass 1). This requires showing that genOracle N false never fails (it skips the collision check) and that the adversary B doesn't cause failure on its own.

source

theorem CatCrypt.Examples.Cryptobox.pkey_switching [CT : CryptoTypes] (N : NIKEScheme) (B : PKEYOracles → Core.SPComp Bool) (coll_bound : ENNReal) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬pkeyBadFinal h' → (PKEY N false B Core.Heap.empty) (some (b, h')) = (PKEY N true B Core.Heap.empty) (some (b, h'))) (hll : Unary.isLossless (PKEY N false B)) (hcoll : (Unary.prEventComp (PKEY N false B) Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => pkeyBadFinal h') ≤ coll_bound) :

pkeyAdvantage N B ≤ coll_bound

PKEY switching as a game hop: when the two PKEY games agree off the collision event pkeyBadFinal, the collision-free game is lossless, and the probability of pkeyBadFinal in the collision-free game is at most coll_bound, the switching advantage is at most coll_bound. The bound on the collision probability is a hypothesis on the collision-free game; collision_prob_single_query bounds the collision probability of one GEN query and collision_prob_multi_query_bound evaluates the union-bound sum over the queries.

Collision-Flag Instrumented Game Infrastructure #

The pkeyBadFinal bad event (∃ pk, honest[pk] ∧ corrupt[pk]) is insufficient for a precise FEL argument because genOracle N true also fails on duplicate honest keys, not just honest-corrupt cross collisions.

We introduce an instrumented variant of the PKEY game that explicitly sets a collision flag whenever the generated pk collides with ANY existing key (honest or corrupt). This gives a stronger, more precise bad event for FEL.

source

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.pkeyCollFlag :

Core.Location

Collision flag location. Set to true when a GEN call produces a pk that collides with an existing honest or corrupt key.

Equations

CatCrypt.Examples.Cryptobox.pkeyCollFlag = { id := 103, ty := Bool, fintype := Bool.fintype, inhabited := instInhabitedBool }

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.genOracle_instr [CT : CryptoTypes] (N : NIKEScheme) (b : Bool) :

Core.SPComp CryptoTypes.PK

Instrumented GEN oracle: like genOracle but sets pkeyCollFlag on collision.

When a collision is detected (the newly generated pk is already honest or corrupt):

Always sets the collision flag to true
If b = true: fails (collision-checking mode)
If b = false: continues without failing (non-collision-checking mode)

When no collision is detected: both b = true and b = false execute identically.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CatCrypt.Examples.Cryptobox.pkeyBadInstr (h : Core.Heap) :

Prop

Instrumented bad event: the collision flag is set.

This is a precise characterization of "some GEN call produced a collision during execution", unlike pkeyBadFinal which only captures the weaker condition of a pk being both honest and corrupt simultaneously.

Equations

CatCrypt.Examples.Cryptobox.pkeyBadInstr h = (h.get CatCrypt.Examples.Cryptobox.pkeyCollFlag = true)

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.PKEY_instr [CT : CryptoTypes] (N : NIKEScheme) (b : Bool) (A : PKEYOracles → Core.SPComp Bool) :

Core.SPComp Bool

Instrumented PKEY game: uses genOracle_instr instead of genOracle.

All other oracles (CSETPK, GETSK, HONPK) are unchanged.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.pkeyOracles_instr_cc [CT : CryptoTypes] (N : NIKEScheme) :

PKEYOracles

Instrumented oracle records for convenience.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.pkeyOracles_instr_nocc [CT : CryptoTypes] (N : NIKEScheme) :

PKEYOracles

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CatCrypt.Examples.Cryptobox.pkeyAdvantage_instr [CT : CryptoTypes] (N : NIKEScheme) (A : PKEYOracles → Core.SPComp Bool) :

ENNReal

Instrumented PKEY advantage.

Equations

CatCrypt.Examples.Cryptobox.pkeyAdvantage_instr N A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Cryptobox.PKEY_instr N false A) (CatCrypt.Examples.Cryptobox.PKEY_instr N true A)

Instances For

source

theorem CatCrypt.Examples.Cryptobox.genOracle_instr_unfold [CT : CryptoTypes] (N : NIKEScheme) (b : Bool) :

genOracle_instr N b = do let pair ← N.pkgen have pk : CryptoTypes.PK := pair.1 have sk : CryptoTypes.SK := pair.2 let honest ← Core.SPComp.get pkHonestLoc let corrupt ← Core.SPComp.get pkCorruptLoc have __do_jp : Unit → Core.SPComp CryptoTypes.PK := fun (__r : Unit) => do let skMap ← Core.SPComp.get skStoreLoc Core.SPComp.set pkHonestLoc (Function.update honest pk true) Core.SPComp.set skStoreLoc (Function.update skMap pk sk) Core.SPComp.pure pk if (honest pk || corrupt pk) = true then do Core.SPComp.set pkeyCollFlag true if b = true then do let __r ← Core.SPComp.fail __do_jp __r else do let __r ← Core.SPComp.pure () __do_jp __r else do let __r ← Core.SPComp.pure () __do_jp __r

Unfolding lemma for genOracle_instr.

Key Theorem: Instrumented Oracles Agree When No Collision #

When the collision flag is NOT set in the final heap, the collision branch was never taken during execution. Therefore, genOracle_instr N false and genOracle_instr N true produce identical distributions on non-bad outcomes.

For any outcome (pk, h') with ¬pkeyBadInstr h' (i.e., Heap.get h' pkeyCollFlag ≠ true):

Both genOracle_instr N false and genOracle_instr N true begin identically: sample pair ← N.pkgen, read honest, corrupt.

At the distribution level, the result at outcome (pk, h') is a sum over intermediate states:

(genOracle_instr N b h₀)(some (pk, h')) =
  ∑_{pair, h₁} (N.pkgen h₀)(some (pair, h₁)) *
    (rest_b pair.1 pair.2 h₁)(some (pk, h'))

For each intermediate (pair, h₁), let pk_gen = pair.1. Read honest = Heap.get h₁ pkHonestLoc and corrupt = Heap.get h₁ pkCorruptLoc.
Case: honest pk_gen || corrupt pk_gen = true (collision detected):
- Both variants set pkeyCollFlag := true in the heap.
- The b = true variant then calls SPComp.fail, producing 0 mass.
- The b = false variant continues and produces h' with pkeyCollFlag = true.
- But we assumed ¬pkeyBadInstr h', i.e., Heap.get h' pkeyCollFlag ≠ true.
- The collision flag, once set to true, persists through subsequent set calls on OTHER locations (pkHonestLoc, skStoreLoc have different ids: 100, 101 vs 103).
- So Heap.get h' pkeyCollFlag = true, contradicting ¬pkeyBadInstr h'.
- Conclusion: this intermediate contributes 0 mass for BOTH b = false and b = true.
Case: honest pk_gen || corrupt pk_gen = false (no collision):
- Both variants execute SPComp.pure (), then identically update the heap.
- The rest of the computation is b-independent.
- Conclusion: identical contribution for both b = false and b = true.
Therefore, every term in the sum is equal, so the total is equal.

source

theorem CatCrypt.Examples.Cryptobox.spcomp_fail_bind {α β : Type} (f : α → Core.SPComp β) :

Core.SPComp.fail.bind f = Core.SPComp.fail

source

theorem CatCrypt.Examples.Cryptobox.spcomp_bind_congr_left {α β : Type} {c₁ c₂ : Core.SPComp α} (f : α → Core.SPComp β) (h : c₁ = c₂) :

c₁.bind f = c₂.bind f

source

theorem CatCrypt.Examples.Cryptobox.collFlag_preserved_by_set (h₁ : Core.Heap) (l : Core.Location) (v : l.ty) (hid : l.id ≠ pkeyCollFlag.id) (hset : h₁.get pkeyCollFlag = true) :

(h₁.set l v).get pkeyCollFlag = true

source

theorem CatCrypt.Examples.Cryptobox.genOracle_instr_agree [CT : CryptoTypes] (N : NIKEScheme) (h₀ : Core.Heap) (pk : CryptoTypes.PK) (h' : Core.Heap) :

¬pkeyBadInstr h' → (genOracle_instr N false h₀) (some (pk, h')) = (genOracle_instr N true h₀) (some (pk, h'))

source

theorem CatCrypt.Examples.Cryptobox.pkeyAdvantage_instr_le_collision [CT : CryptoTypes] (N : NIKEScheme) (B : PKEYOracles → Core.SPComp Bool) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬pkeyBadInstr h' → (PKEY_instr N false B Core.Heap.empty) (some (b, h')) = (PKEY_instr N true B Core.Heap.empty) (some (b, h'))) (hll : Unary.isLossless (PKEY_instr N false B)) :

pkeyAdvantage_instr N B ≤ Unary.prEventComp (PKEY_instr N false B) Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => pkeyBadInstr h'

PKEY instrumented advantage bounded by collision probability via FEL.

This is the instrumented analogue of pkeyAdvantage_le_collision. The stronger bad event pkeyBadInstr (collision flag set) gives a tighter and more precise bound than pkeyBadFinal (honest-corrupt overlap).

source

theorem CatCrypt.Examples.Cryptobox.pkeyBadInstr_implies_flag_set (h : Core.Heap) :

pkeyBadInstr h → h.get pkeyCollFlag = true

The instrumented bad event implies the original bad event when there exists a key that is both honest and corrupt.

More precisely: if a collision flag was set during a GEN call where honest pk_gen || corrupt pk_gen = true, then either:

The pk was already honest, and GEN sets it honest again (duplicate honest key)
The pk was already corrupt, and GEN sets it honest (honest-corrupt overlap → pkeyBadFinal)

Note: pkeyBadInstr is STRICTLY stronger than pkeyBadFinal because it also catches duplicate honest-honest collisions.

Per-Query Collision Probability #

For a single GEN query, the probability that the newly sampled pk collides with existing keys depends on the number of already-registered keys and the size of the pk space.

source

theorem CatCrypt.Examples.Cryptobox.collision_prob_single_query [CT : CryptoTypes] (h₀ : Core.Heap) (q_existing : ℕ) (h_count : ∃ (S : Finset CryptoTypes.PK), S.card = q_existing ∧ ∀ (pk : CryptoTypes.PK), h₀.get pkHonestLoc pk = true ∨ h₀.get pkCorruptLoc pk = true → pk ∈ S) :

Crypto.prTrue ((Core.SPComp.sample CryptoTypes.PK).bind fun (pk : CryptoTypes.PK) => Core.SPComp.pure (decide (pk ∈ {p : CryptoTypes.PK | h₀.get pkHonestLoc p = true ∨ h₀.get pkCorruptLoc p = true}))) h₀ ≤ ↑q_existing / ↑(Fintype.card CryptoTypes.PK)

Per-query collision probability bound.

The collision set on heap h₀ is the set of pk whose pkHonestLoc or pkCorruptLoc flag is set. If it is covered by a finset S of size q_existing, then a public key sampled uniformly from CT.PK lands in the collision set with probability at most q_existing / Fintype.card CT.PK. This is the per-GEN-query collision probability under uniform key generation.

source

theorem CatCrypt.Examples.Cryptobox.collision_prob_multi_query_bound [CT : CryptoTypes] (q_gen q_csetpk : ℕ) :

∑ i ∈ Finset.range q_gen, (↑i + ↑q_csetpk) / ↑(Fintype.card CryptoTypes.PK) = ↑(q_gen * (q_gen - 1) + 2 * (q_gen * q_csetpk)) / (2 * ↑(Fintype.card CryptoTypes.PK))

Multi-query collision bound via union bound.

With q_gen GEN queries, the i-th of which (0-indexed) has at most i existing challenger-generated keys plus q_csetpk corrupt keys, the union bound over the per-query collision probabilities is the sum ∑_{i=0}^{q_gen-1} (i + q_csetpk) / |PK|. This sum equals the birthday closed form (q_gen * (q_gen - 1) + 2 * (q_gen * q_csetpk)) / (2 * |PK|).

Standalone PKEY sdist Building Block #

source

theorem CatCrypt.Examples.Cryptobox.pkey_sdist [CT : CryptoTypes] (N : NIKEScheme) (ε : ENNReal) (h : ∀ (A : PKEYOracles → Core.SPComp Bool), pkeyAdvantage N A ≤ ε) :

Crypto.sdist (PKEY N false) (PKEY N true) ≤ ε

Standalone PKEY sdist building block. Reusable by any construction that uses the PKEY game.

Bridges per-adversary advantage bounds (∀ A, pkeyAdvantage N A ≤ ε) to categorical sdist (sdist (PKEY N false) (PKEY N true) ≤ ε), giving access to PPLs, composition, and tensor bounds.

Documentation

CatCryptCore.Examples.Cryptobox.PKEY

PKEY: Public Key Management Game #

Overview #

References #

Heap Locations #

Oracle Definitions #

Oracle Record #

PKEY Game #

PKEY Collision Analysis #

Proof Structure #

Comparison with Other Formalizations #

genOracle Analysis #

PKEY FEL Application #

Collision-Flag Instrumented Game Infrastructure #

Key Theorem: Instrumented Oracles Agree When No Collision #

Per-Query Collision Probability #

Standalone PKEY sdist Building Block #