AE: Multi-instance Authenticated Encryption Game

The AE game captures the security of authenticated encryption across multiple sessions, composing the KEY game (shared key management) with per-session encryption/decryption.

Overview

Two variants parameterized by b : Bool:

• b = false (real): encrypt and decrypt using the actual shared key from KEY
• b = true (ideal): for honest sessions, encryption returns a random ciphertext (logged per session and nonce), decryption checks the log; for corrupt sessions, real encryption/decryption is used

Oracles

• aenc: Encrypt a message for a session under a nonce
• adec: Decrypt a ciphertext for a session under a nonce

The AE oracles internally query KEY oracles for key retrieval and honesty checks.

References

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

Heap Locations

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

@[reducible]

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

Per-session encryption log: maps each (SID, Nonce) pair to an optional (plaintext, ciphertext) pair recorded during ideal encryption.

Equations

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

Oracle Definitions

Each oracle retrieves the shared key and honesty flag from the KEY oracles, then behaves either as real encryption/decryption or ideal (log-based) depending on b and the honesty of the session.

noncomputable def CatCrypt.Examples.Cryptobox.aeEncOracle [CT : CryptoTypes] (E : NBSES) (I : KeyInjection) (b : Bool) (keyO : KEYOracles) (sid : SID) (m : CryptoTypes.M) (n : CryptoTypes.Nonce) : Core.SPComp CryptoTypes.C

AE encryption oracle.

• Gets the shared key for the session via keyO.kget
• Checks honesty via keyO.khon
• If b = false (real): encrypt with E.enc (I.encode k) m n
• If b = true AND the session is honest: sample a random ciphertext, log the (message, ciphertext) pair at (sid, n)
• If b = true but the session is corrupt: real encryption

Equations

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

noncomputable def CatCrypt.Examples.Cryptobox.aeDecOracle [CT : CryptoTypes] (E : NBSES) (I : KeyInjection) (b : Bool) (keyO : KEYOracles) (sid : SID) (c : CryptoTypes.C) (n : CryptoTypes.Nonce) : Core.SPComp (Option CryptoTypes.M)

AE decryption oracle.

• Gets the shared key for the session via keyO.kget
• Checks honesty via keyO.khon
• If b = false (real): decrypt with E.dec (I.encode k) c n
• If b = true AND the session is honest: look up (sid, n) in the log; if the ciphertext matches the logged one, return the logged plaintext; otherwise return none
• If b = true but the session is corrupt: real decryption

Equations

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

Oracle Record

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

Oracle interface for AE games.

• aenc : SID → CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C
• adec : SID → CryptoTypes.C → CryptoTypes.Nonce → Core.SPComp (Option CryptoTypes.M)

AE Game

The AE game composes KEY oracles internally: the adversary gets access to both AE oracles (encrypt/decrypt) and KEY oracles (key management).

noncomputable def CatCrypt.Examples.Cryptobox.GAE [CT : CryptoTypes] (E : NBSES) (I : KeyInjection) (b : Bool) (keyO : KEYOracles) (A : AEOracles → Core.SPComp Bool) : Core.SPComp Bool

AE game parameterized by real/ideal behavior b.

• b = false: real — encrypt/decrypt with actual shared keys
• b = true: ideal — honest sessions use random ciphertexts and log-based decryption; corrupt sessions still use real encryption

The adversary receives both AE oracles and KEY oracles.

Equations

• CatCrypt.Examples.Cryptobox.GAE E I b keyO A = A { aenc := CatCrypt.Examples.Cryptobox.aeEncOracle E I b keyO, adec := CatCrypt.Examples.Cryptobox.aeDecOracle E I b keyO }

AE Advantage

noncomputable def CatCrypt.Examples.Cryptobox.aeAdvantage [CT : CryptoTypes] (E : NBSES) (I : KeyInjection) (keyO : KEYOracles) (A : AEOracles → Core.SPComp Bool) : ENNReal

AE advantage: distinguishing distance between real and ideal AE games with fixed KEY oracles.

Equations

• CatCrypt.Examples.Cryptobox.aeAdvantage E I keyO A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Cryptobox.GAE E I false keyO A) (CatCrypt.Examples.Cryptobox.GAE E I true keyO A)