AE Hybrid Argument for Cryptobox

Hybrid games for the AE switching step in the Cryptobox security proof. The AE step transitions session-by-session from real encryption (with random shared keys) to ideal encryption (random ciphertext + log-based decryption).

Overview

The aeStepAdvantage from GameHopping.lean captures the distance:

  Advantage(PKAE_nikeSwitch, PKAE_cc(true))

We decompose this via a hybrid argument over sessions. The hybrid game aeHybrid S is parameterized by a set S : Finset SID of "switched" sessions:

• Sessions in S: ideal encryption (random ciphertext, log-based decryption)
• Sessions not in S: real encryption (with random cached key from getOrSampleKey)
• Corrupt sessions: always real encryption (with N.sharedkey)

Boundary conditions

• aeHybrid_empty : aeHybrid N E I {} A = PKAE_nikeSwitch N E I A
• aeHybrid_univ : aeHybrid N E I Finset.univ A = PKAE_cc N E I true A

Per-step structure

Each step switches a single session sid from real to ideal:

  Advantage(aeHybrid(S), aeHybrid(S ∪ {sid})) ≤ saeAdvantage E (R_sae sid A)

Main results

• aeHybrid - Hybrid game parameterized by switched session set
• aeHybridStepAdvantage - Per-step advantage for switching one session
• aeHybrid_empty - Boundary: aeHybrid {} = PKAE_nikeSwitch
• aeHybrid_univ - Boundary: aeHybrid univ = PKAE_cc true
• aeStep_triangle - AE step advantage bounded by sum over hybrid steps

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

Hybrid Encryption Oracle

The encryption oracle for the hybrid game. Parameterized by a set of switched sessions S : Finset SID. For honest-honest sessions in S, we use ideal encryption (sample random ciphertext + log). For honest-honest sessions NOT in S, we use real encryption with a random cached key. For corrupt sessions, we always use real encryption with the actual NIKE shared key.

noncomputable def CatCrypt.Examples.Cryptobox.aeHybridEncOracle [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (switched : Finset SID) (pkeyO : PKEYOracles) (pk_s pk_r : CryptoTypes.PK) (m : CryptoTypes.M) (n : CryptoTypes.Nonce) : Core.SPComp CryptoTypes.C

Hybrid encryption oracle parameterized by switched session set.

• Honest-honest sessions in switched: ideal (sample random ciphertext, log it)
• Honest-honest sessions not in switched: real (random cached key + E.enc)
• Corrupt sessions: real (N.sharedkey + E.enc)

Equations

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

Hybrid Decryption Oracle

The decryption oracle for the hybrid game, following the same switching logic as encryption.

noncomputable def CatCrypt.Examples.Cryptobox.aeHybridDecOracle [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (switched : Finset SID) (pkeyO : PKEYOracles) (pk_r pk_s : CryptoTypes.PK) (c : CryptoTypes.C) (n : CryptoTypes.Nonce) : Core.SPComp (Option CryptoTypes.M)

Hybrid decryption oracle parameterized by switched session set.

• Honest-honest sessions in switched: ideal (log-based decryption)
• Honest-honest sessions not in switched: real (random cached key + E.dec)
• Corrupt sessions: real (N.sharedkey + E.dec)

Equations

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

Hybrid Game

The hybrid game composes the collision-checking PKEY oracles with the hybrid encryption/decryption oracles.

noncomputable def CatCrypt.Examples.Cryptobox.aeHybrid [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (switched : Finset SID) (A : PKAEOracles → Core.SPComp Bool) : Core.SPComp Bool

AE hybrid game parameterized by switched session set S.

Uses collision-checking GEN (matching PKAE_cc) and routes encryption/decryption through the hybrid oracles. The set S controls which honest-honest sessions use ideal encryption:

• S = {}: all honest sessions use real encryption (= PKAE_nikeSwitch)
• S = Finset.univ: all honest sessions use ideal encryption (= PKAE_cc true)

Equations

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

Boundary Theorems

The hybrid game at the two extremes matches the existing game definitions.

theorem CatCrypt.Examples.Cryptobox.aeHybrid_empty [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) : aeHybrid N E I ∅ A = PKAE_nikeSwitch N E I A

Empty boundary: when no session is switched, the hybrid game equals PKAE_nikeSwitch — all honest-honest sessions use real encryption with random cached keys.

Proof strategy: When switched = {}, the condition sid ∈ switched is always false, so the hybrid oracles always take the "real" branch. The real branch of the hybrid enc/dec oracles uses getOrSampleKey + E.enc/E.dec, which matches PKAE_nikeSwitch.

theorem CatCrypt.Examples.Cryptobox.aeHybrid_univ [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) : aeHybrid N E I Finset.univ A = PKAE_cc N E I true A

Universe boundary: when all sessions are switched, the hybrid game equals PKAE_cc true — all honest-honest sessions use ideal encryption.

Proof strategy: When switched = Finset.univ, the condition sid ∈ switched is always true for any sid, so the hybrid oracles always take the "ideal" branch for honest-honest sessions. The ideal branch matches pkaeEncOracle/ pkaeDecOracle with b = true.

The only subtlety is that PKAE_cc true uses pkaeEncOracle which checks b && hon_s && hon_r while the hybrid oracle checks hon_s && hon_r then sid ∈ switched. When switched = univ and both are honest, both branches produce the same ideal behavior. When either party is corrupt, both fall through to the real encryption with N.sharedkey.

Per-Step Advantage

The advantage of switching a single session from real to ideal encryption.

noncomputable def CatCrypt.Examples.Cryptobox.aeHybridStepAdvantage [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (S : Finset SID) (sid : SID) (A : PKAEOracles → Core.SPComp Bool) : ENNReal

Per-step advantage: the distinguishing distance when adding session sid to the switched set.

This captures the cost of switching one session from real to ideal encryption. The reduction to single-instance SAE (saeAdvantage) requires showing that the per-session difference can be simulated by a single SAE adversary.

Equations

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

theorem CatCrypt.Examples.Cryptobox.aeHybridStepAdvantage_mem [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (S : Finset SID) (sid : SID) (A : PKAEOracles → Core.SPComp Bool) (hmem : sid ∈ S) : aeHybridStepAdvantage N E I S sid A = 0

When sid ∈ S, inserting sid again does nothing, so the step advantage is 0.

Proof strategy: insert sid S = S when sid ∈ S, so the two hybrid games are definitionally equal.

SAE Reduction Adversary

The reduction adversary that converts a single-session SAE attacker into a PKAE hybrid distinguisher. When the SAE game provides real encryption, we get aeHybrid S; when it provides ideal encryption, we get aeHybrid (insert sid S).

noncomputable def CatCrypt.Examples.Cryptobox.R_SAE_hybrid [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (switched : Finset SID) (targetSid : SID) (A : PKAEOracles → Core.SPComp Bool) : SAEOracles → Core.SPComp Bool

SAE reduction adversary for the hybrid step.

Given SAE oracles for a single session, constructs PKAE oracles where:

• Session sid: routes through SAE oracles (real or ideal depending on SAE game)
• Other sessions in switched: ideal encryption (random ciphertext + log)
• Other sessions not in switched: real encryption (random cached key)
• Corrupt sessions: real encryption (N.sharedkey)

When plugged into SAE(false), this gives aeHybrid S. When plugged into SAE(true), this gives aeHybrid (insert sid S).

This captures the core of the hybrid argument: the per-step advantage is bounded by the SAE advantage of this reduction adversary.

Equations

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

Hybrid Step Bound

The per-step advantage is bounded by the SAE advantage of the reduction.

theorem CatCrypt.Examples.Cryptobox.aeHybrid_step_bound [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (S : Finset SID) (sid : SID) (_hns : sid ∉ S) (A : PKAEOracles → Core.SPComp Bool) (h_real : aeHybrid N E I S A = SAE E false (R_SAE_hybrid N E I S sid A)) (h_ideal : aeHybrid N E I (insert sid S) A = SAE E true (R_SAE_hybrid N E I S sid A)) : aeHybridStepAdvantage N E I S sid A ≤ saeAdvantage E (R_SAE_hybrid N E I S sid A)

Per-step reduction: the hybrid step advantage for session sid is bounded by the SAE advantage of the reduction adversary R_SAE_hybrid.

The two oracle alignment hypotheses capture the core of the reduction:

• h_real: when SAE provides real encryption, the composed game equals the hybrid game without sid switched
• h_ideal: when SAE provides ideal encryption, the composed game equals the hybrid game with sid switched

Proving these alignments requires showing that routing the target session through SAE oracles produces identical distributions to the hybrid oracles. The main subtlety is aligning the SAE log (indexed by nonce) with the PKAE log (indexed by (SID, Nonce)) for the target session.

Triangle Inequality over Hybrid Chain

Decomposing the AE step advantage into a sum of per-step advantages.

theorem CatCrypt.Examples.Cryptobox.aeHybrid_union_triangle [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (S : Finset SID) (sids : List SID) (hnodup : sids.Nodup) (hdisjoint : ∀ sid ∈ sids, sid ∉ S) : Crypto.Advantage (aeHybrid N E I S A) (aeHybrid N E I (S ∪ sids.toFinset) A) ≤ (List.map (fun (sid : SID) => aeHybridStepAdvantage N E I (S ∪ (List.takeWhile (fun (x : SID) => decide (x ≠ sid)) sids).toFinset) sid A) sids).sum

Auxiliary: advantage of switching from S to S ∪ T is bounded by the sum of advantages of inserting each element of T one at a time.

This follows from the triangle inequality applied iteratively: Advantage(aeHybrid S, aeHybrid (S ∪ T)) ≤ Σ_{sid ∈ T} Advantage(aeHybrid S_i, aeHybrid S_{i+1}) where S_0 = S and S_{i+1} = insert t_i S_i.

theorem CatCrypt.Examples.Cryptobox.aeStep_triangle [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (sids : List SID) (hnodup : sids.Nodup) (hcomplete : sids.toFinset = Finset.univ) : aeStepAdvantage N E I A ≤ (List.map (fun (sid : SID) => aeHybridStepAdvantage N E I (List.takeWhile (fun (x : SID) => decide (x ≠ sid)) sids).toFinset sid A) sids).sum

AE step triangle inequality: the AE step advantage (from PKAE_nikeSwitch to PKAE_cc true) is bounded by the sum of per-step hybrid advantages over all sessions.

Combined with aeHybrid_step_bound, this gives: aeStepAdvantage ≤ Σ_{sid} saeAdvantage E (R_SAE_hybrid ... sid A)

Proof strategy:

1. Rewrite PKAE_nikeSwitch = aeHybrid ∅ via aeHybrid_empty
2. Rewrite PKAE_cc true = aeHybrid Finset.univ via aeHybrid_univ
3. Apply aeHybrid_union_triangle with S = ∅ and sids = all sessions
4. Simplify ∅ ∪ sids.toFinset = Finset.univ

Combined Bound

Putting together the triangle inequality and per-step SAE reduction.

theorem CatCrypt.Examples.Cryptobox.aeStep_bounded_by_sae [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (sids : List SID) (hnodup : sids.Nodup) (hcomplete : sids.toFinset = Finset.univ) (sae_eps : SID → ENNReal) (h_oracle_align : ∀ (S : Finset SID), ∀ sid ∉ S, aeHybrid N E I S A = SAE E false (R_SAE_hybrid N E I S sid A) ∧ aeHybrid N E I (insert sid S) A = SAE E true (R_SAE_hybrid N E I S sid A)) (hsteps : ∀ sid ∈ sids, saeAdvantage E (R_SAE_hybrid N E I (List.takeWhile (fun (x : SID) => decide (x ≠ sid)) sids).toFinset sid A) ≤ sae_eps sid) : aeStepAdvantage N E I A ≤ (List.map sae_eps sids).sum

AE hybrid bound: the AE step advantage is bounded by the sum of SAE advantages of the per-session reduction adversaries.

This is the main result of the hybrid argument:

  aeStepAdvantage N E I A ≤ Σ_{sid} saeAdvantage E (R_SAE_hybrid ... sid A)

Combined with cryptobox_security_full from GameHopping.lean, this gives the complete Cryptobox security bound.

Finset-Based Bound (Alternative Formulation)

An alternative formulation using Finset.sum instead of List.map ... .sum, which is sometimes more convenient for downstream use.

theorem CatCrypt.Examples.Cryptobox.aeStep_bounded_by_sae_finset [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (sae_eps : SID → ENNReal) (hsteps : ∀ (S : Finset SID), ∀ sid ∉ S, aeHybridStepAdvantage N E I S sid A ≤ sae_eps sid) : aeStepAdvantage N E I A ≤ Finset.univ.sum sae_eps

AE hybrid bound (Finset version): the AE step advantage is bounded by the sum of per-session SAE advantages over all sessions.

This takes the per-step bounds as hypotheses, matching the structure of ae_hybrid_bound from Cryptobox.lean.