PKAE: Public-Key Authenticated Encryption Game

The PKAE game is the target security definition for Cryptobox. It captures the combined security of NIKE + NBSES as a public-key authenticated encryption scheme.

Overview

Two variants parameterized by b : Bool:

• b = false (real): encryption and decryption use the actual shared key derived from the NIKE scheme
• b = true (ideal): for honest-honest sessions, encryption returns a uniformly random ciphertext (logging the query), and decryption checks the log instead of decrypting; for pairs involving a corrupt key, the real scheme is used

The PKAE game internally creates PKEY oracles (with collision-free = true) for key management, and provides additional encryption/decryption oracles.

Oracles

• pgen: Generate an honest key pair (delegates to PKEY GEN)
• pcsetpk: Register a corrupt public key (delegates to PKEY CSETPK)
• penc: Encrypt a message from sender to receiver under a nonce
• pdec: Decrypt a ciphertext from sender to receiver under a nonce

References

• Rocq SSProve: theories/Cryptobox/PKAE.v
• Dupressoir et al., CSF 2022 (Section 4.4)

Heap Locations

State specific to the PKAE game. Location IDs start at 500 to avoid collisions with PKEY (100-range), KEY (200-range), SAE (300-range), and NIKE (400-range) locations.

@[reducible]

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

Encryption log indexed by (PK, PK, Nonce): maps each (sender, receiver, nonce) triple to an optional (M, C) pair recorded during ideal encryption. Used in the ideal game to answer decryption queries consistently.

Equations

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

Oracle Definitions

Each oracle is an SPComp computation that reads/writes heap locations. The b : Bool parameter switches between real and ideal behavior for encryption and decryption.

noncomputable def CatCrypt.Examples.Cryptobox.PKAEGame.pkaeEncOracle [CT : CryptoTypes] (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.

Given sender and receiver public keys, a message, and a nonce:

1. Retrieve the sender's secret key via pkeyO.getsk
2. Check honesty of both parties via pkeyO.honpk
3. If both honest AND b = true (ideal): sample a random ciphertext, log the (message, ciphertext) pair, and return the ciphertext
4. Otherwise (real, or at least one corrupt): compute the shared key via N.sharedkey, apply key injection, and encrypt with E.enc

Equations

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

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

PKAE decryption oracle.

Given sender and receiver public keys, a ciphertext, and a nonce:

1. Retrieve the receiver's secret key via pkeyO.getsk
2. Check honesty of both parties via pkeyO.honpk
3. If both honest AND b = true (ideal): look up the encryption log for the reverse direction (pk_r, pk_s, n):
   • If found and the ciphertext matches: return the logged plaintext
   • Otherwise: return none (no decryption in ideal world for ciphertexts not produced by the encryption oracle)
4. Otherwise (real, or at least one corrupt): compute the shared key via N.sharedkey, apply key injection, and decrypt with E.dec

Equations

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

Oracle Record

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

Oracle interface for PKAE games. Provides key generation, corrupt key registration, encryption, and decryption oracles.

• pgen : Unit → Core.SPComp CryptoTypes.PK

  Generate a fresh honest key pair

• pcsetpk : CryptoTypes.PK → Core.SPComp Unit

  Register an adversary-chosen public key as corrupt

• penc : CryptoTypes.PK → CryptoTypes.PK → CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C

  Encrypt: sender PK, receiver PK, message, nonce → ciphertext

• pdec : CryptoTypes.PK → CryptoTypes.PK → CryptoTypes.C → CryptoTypes.Nonce → Core.SPComp (Option CryptoTypes.M)

  Decrypt: sender PK, receiver PK, ciphertext, nonce → optional message

PKAE Game

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

PKAE game parameterized by b:

• b = false: real — encrypt/decrypt with actual NIKE shared keys
• b = true: ideal — honest-honest encryption returns random ciphertext, decryption checks log; corrupt sessions use real keys

Internally creates PKEY oracles with collision-free = true, which is justified by the PKEY switching lemma.

Equations

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

PKAE Advantage

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

Advantage of the GPKAE game: the distinguishing distance between its real and ideal variants.

This is a different game from the one measured by CatCrypt.Examples.Cryptobox.pkaeAdvantage (module Cryptobox), which the Cryptobox hop chain (pkae_game_hopping) bounds. The two games differ in three respects: GPKAE runs the collision-checking key oracle (genOracle N true) where Cryptobox.PKAE runs genOracle N false; its oracle record (PKAEGame.PKAEOracles) exposes only key generation, corruption, encryption and decryption, without the getsk and honpk oracles; and its log is indexed by the ordered pair (pk_s, pk_r, n) where Cryptobox.PKAE uses the sorted session identifier. No equation between the two advantages is proved.

Equations

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