Cryptobox: Main Security Theorem

This file states the main security theorem for the Cryptobox construction (NaCl's crypto_box), which combines a Non-Interactive Key Exchange (NIKE, e.g., X25519) with a Nonce-Based Symmetric Encryption Scheme (NBSES, e.g., XSalsa20-Poly1305) to achieve Public-Key Authenticated Encryption (PKAE).

Game-hopping chain

The proof proceeds by a sequence of game hops:

  G0: PKAE(real)
    = PKEY(0) ∘ NIKE(0) ∘ KEY(0) ∘ AE(0)     -- decomposition
  ≈ PKEY(1) ∘ NIKE(0) ∘ KEY(0) ∘ AE(0)       -- Step 1: PKEY switching (FEL)
  ≈ PKEY(1) ∘ NIKE(1) ∘ KEY(0) ∘ AE(0)       -- Step 2: NIKE reduction
    = PKEY(1) ∘ NIKE(1) ∘ KEY(1) ∘ AE(0)     -- Step 3: KEY(0) = KEY(1) (structural)
  ≈ PKEY(1) ∘ NIKE(1) ∘ KEY(1) ∘ AE(1)       -- Step 4: AE hybrid argument
    = PKAE(ideal)                              -- recomposition

Advantage bound

  Adv[PKAE] ≤ Adv[PKEY] + Adv[NIKE] + Adv[AE]
            ≤ 2 · q_gen · q_csetpk · (1 / |PK|)    -- FEL collision bound
              + nike_eps                              -- NIKE advantage
              + Σ_{i < q} sae_eps(i)                 -- hybrid sum of SAE advantages

Architecture

The hdecomp hypothesis in the main theorem corresponds to the three structural equivalences that are ADMITTED in the Rocq SSProve formalization:

1. PKAE(real) decomposes into PKEY(0) ∘ NIKE(0) ∘ KEY(0) ∘ AE(0)
2. PKAE(ideal) decomposes into PKEY(1) ∘ NIKE(1) ∘ KEY(1) ∘ AE(1)
3. KEY(0) = KEY(1) structurally

Given these decompositions (taken as hypotheses), the security bound follows from the triangle inequality and monotonicity of addition — which we prove.

Improved Version

The cryptobox_security_full theorem in GameHopping.lean improves on cryptobox_security by:

• Proving the PKEY reductions (not hypothesized) via definitional equality
• Decomposing into 4 independent, transparent proof obligations (h_pkey_real, h_pkey_ideal, h_nike, h_ae)
• Making the game-hopping chain explicit with intermediate games

Relationship

  cryptobox_security       -- monolithic hdecomp hypothesis (this file)
  cryptobox_security_full  -- 4 independent hypotheses, PKEY proven (GameHopping.lean)
    ← cryptobox_security_chain  -- 3-step game-hopping with triangle inequality
      ← pkae_game_hopping       -- PKEY reductions proven by definitional equality
        ← PKAE_eq_PKEY_nocheck  -- PKAE = PKEY(no-check) ∘ R_PKEY (by rfl)
        ← PKAE_cc_eq_PKEY_check -- PKAE_cc = PKEY(check) ∘ R_PKEY (by rfl)

GameHopping.lean composes the full hop chain (cryptobox_security_full).

References

• Dupressoir et al., "Bringing SSP to EasyCrypt — A Security Proof for Cryptobox" (CSF 2022)
• Dupressoir et al., "How Hard Can It Be?" (ASIACRYPT 2025)
• Myssenburg et al., Rocq SSProve Cryptobox (nominal-ssprove)
• Bernstein, Lange, Schwabe, "NaCl: Networking and Cryptography library"

PKAE Oracle Interface

The target security notion. The PKAE game gives the adversary access to PKEY oracles plus encryption/decryption parameterized by b : Bool:

• b = false (real): use the cryptobox construction
• b = true (ideal): encryption returns random ciphertexts, decryption uses a log

structure CatCrypt.Examples.Cryptobox.PKAEOracles [CT : CryptoTypes] : Type

Oracle interface for the PKAE game. Combines PKEY oracles with encryption/decryption.

• gen : Unit → Core.SPComp CryptoTypes.PK
• csetpk : CryptoTypes.PK → Core.SPComp Unit
• getsk : CryptoTypes.PK → Core.SPComp CryptoTypes.SK
• honpk : CryptoTypes.PK → Core.SPComp Bool
• enc : CryptoTypes.PK → CryptoTypes.PK → CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C
• dec : CryptoTypes.PK → CryptoTypes.PK → CryptoTypes.C → CryptoTypes.Nonce → Core.SPComp (Option CryptoTypes.M)

PKAE Heap Locations

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.pkaeLogLoc [CT : CryptoTypes] : Core.Location

Per-session encryption log for ideal PKAE, indexed by (SID, Nonce).

Equations

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

PKAE Oracle Definitions

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

PKAE encryption oracle.

• b = false (real): encrypt using the cryptobox construction
• b = true (ideal): sample a random ciphertext and log the pair

Equations

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

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

PKAE decryption oracle.

• b = false (real): decrypt using the cryptobox construction
• b = true (ideal): look up (sid, n) in the log

Equations

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

PKAE Game

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

PKAE game parameterized by b:

• b = false (real): cryptobox construction
• b = true (ideal): random ciphertexts for honest-honest sessions

Equations

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

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

PKAE advantage: distinguishing real from ideal PKAE. This is the advantage that the Cryptobox hop chain bounds. The collision-checking variant with the narrower oracle record, GPKAE in module PKAE, has its own advantage PKAEGame.gpkaeAdvantage.

Equations

• CatCrypt.Examples.Cryptobox.pkaeAdvantage N E I A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Cryptobox.PKAE N E I false A) (CatCrypt.Examples.Cryptobox.PKAE N E I true A)

Reductions

Adversary wrappers that reduce the security of one game to another.

noncomputable def CatCrypt.Examples.Cryptobox.R_GNIKE [CT : CryptoTypes] (_N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) : PKEYOracles → NIKEOracles → Core.SPComp Bool

NIKE reduction: wrap a PKAE adversary into one attacking the NIKE game. Routes encryption/decryption through the NIKE shared key oracle.

Equations

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

noncomputable def CatCrypt.Examples.Cryptobox.R_GSAE [CT : CryptoTypes] (_E : NBSES) (_I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (_i : ℕ) : SAEOracles → Core.SPComp Bool

SAE reduction at hybrid index i: wrap a PKAE adversary into one attacking the single-instance SAE game for session i. Routes session i's encryption/decryption through the SAE oracle.

Equations

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

AE Hybrid Argument

The AE game switches from real to ideal encryption across multiple sessions. This is decomposed via a hybrid argument: switch one session at a time, and bound the total advantage by the sum of per-session SAE advantages.

The i-th hybrid game uses ideal encryption for sessions 0, ..., i-1 and real encryption for sessions i, ..., q-1.

theorem CatCrypt.Examples.Cryptobox.ae_hybrid_bound [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (E : NBSES) (I : KeyInjection) (keyO : KEYOracles) (A : AEOracles → Core.SPComp Bool) (q : ℕ) (sae_eps step_adv : ℕ → ENNReal) (hdecomp : aeAdvantage E I keyO A ≤ (Finset.range q).sum step_adv) (hsteps : ∀ i < q, step_adv i ≤ sae_eps i) : aeAdvantage E I keyO A ≤ (Finset.range q).sum sae_eps

AE advantage bounded by sum of SAE advantages via hybrid argument.

Takes a hybrid decomposition hypothesis hdecomp that decomposes the AE advantage into per-step contributions, and per-step bounds hsteps. The decomposition corresponds to the triangle inequality applied to:

  AE(real) = H(0) ≈ H(1) ≈ ... ≈ H(q) = AE(ideal)

Main Security Theorem

theorem CatCrypt.Examples.Cryptobox.cryptobox_security [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) (A : PKAEOracles → Core.SPComp Bool) (q_gen q_csetpk q : ℕ) (nike_eps : ENNReal) (sae_eps : ℕ → ENNReal) (pkey_adv nike_adv ae_adv : ENNReal) (hdecomp : pkaeAdvantage N E I A ≤ pkey_adv + nike_adv + ae_adv) (hpkey : pkey_adv ≤ 2 * ↑(q_gen * q_csetpk) * (1 / ↑(Fintype.card CryptoTypes.PK))) (hnike : nike_adv ≤ nike_eps) (hae : ae_adv ≤ (Finset.range q).sum sae_eps) : pkaeAdvantage N E I A ≤ 2 * ↑(q_gen * q_csetpk) * (1 / ↑(Fintype.card CryptoTypes.PK)) + nike_eps + (Finset.range q).sum sae_eps

Cryptobox security theorem.

The PKAE advantage of any adversary A against the Cryptobox construction is bounded by the sum of:

1. PKEY switching (FEL collision bound): 2 * q_gen * q_csetpk * (1 / |PK|)

2. NIKE advantage: nike_eps

3. AE hybrid sum: Σ_{i < q} sae_eps(i)

The hdecomp hypothesis encapsulates the game-hopping decomposition:

  PKAE(real) ≈_{PKEY} PKAE' ≈_{NIKE} PKAE'' ≈_{KEY} PKAE''' ≈_{AE} PKAE(ideal)

This corresponds to the three structural equivalences that are ADMITTED in the Rocq SSProve formalization (package decomposition and recomposition).

Given hdecomp, the bound follows from monotonicity of addition.

Instantiation: X25519 + XSalsa20-Poly1305

For concrete security, one would instantiate:

• CT.PK = CT.SK = Fin (2^255 - 19) (Curve25519 points)
• CT.SharedKey = Fin (2^256) (HSalsa20 output)
• N.sharedkey = X25519
• E.enc/dec = XSalsa20-Poly1305
• I.encode = HSalsa20

The NIKE advantage reduces to the CDH assumption on Curve25519. The SAE advantage reduces to the PRF security of XSalsa20 and the MAC security of Poly1305.

These concrete instantiations are left for future work.