SAE: Single-instance Authenticated Encryption Game

The SAE game captures the security of a single symmetric encryption instance, parameterized by a Nonce-Based Symmetric Encryption Scheme (NBSES).

Overview

Two variants parameterized by b : Bool:

• b = false (real): encrypt and decrypt using the actual shared key
• b = true (ideal): encryption returns a random ciphertext (and logs the plaintext-ciphertext pair), decryption checks the log instead of using the key

Oracles

• sgen: Generate and store a random shared key
• senc: Encrypt a message under a nonce (real or ideal)
• sdec: Decrypt a ciphertext under a nonce (real or log-based)

References

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

Heap Locations

State is stored in the global heap via typed locations. Locations are @[reducible] so that .ty reduces for type checking.

@[reducible]

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

The single shared encryption key.

Equations

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

@[reducible]

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

Encryption log indexed by nonce: maps each nonce to an optional (plaintext, ciphertext) pair recorded during ideal encryption.

Equations

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

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.saeInitLoc : Core.Location

Whether the key has been generated.

Equations

• CatCrypt.Examples.Cryptobox.saeInitLoc = { id := 302, ty := Bool, fintype := Bool.fintype, inhabited := instInhabitedBool }

Oracle Definitions

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

noncomputable def CatCrypt.Examples.Cryptobox.saeGenOracle [CT : CryptoTypes] (_E : NBSES) : Core.SPComp Unit

SGEN oracle: generate and store a fresh random shared key. Fails if the key has already been generated.

Equations

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

noncomputable def CatCrypt.Examples.Cryptobox.saeEncOracle [CT : CryptoTypes] (E : NBSES) (b : Bool) (m : CryptoTypes.M) (n : CryptoTypes.Nonce) : Core.SPComp CryptoTypes.C

SENC oracle: encrypt a message under a nonce.

• b = false (real): encrypt with the stored key
• b = true (ideal): sample a random ciphertext, log the (message, ciphertext) pair at the given nonce; fails if the nonce was already used (honesty check)

Equations

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

noncomputable def CatCrypt.Examples.Cryptobox.saeDecOracle [CT : CryptoTypes] (E : NBSES) (b : Bool) (c : CryptoTypes.C) (n : CryptoTypes.Nonce) : Core.SPComp (Option CryptoTypes.M)

SDEC oracle: decrypt a ciphertext under a nonce.

• b = false (real): decrypt with the stored key
• b = true (ideal): look up the nonce in the log; if the ciphertext matches the logged one, return the logged plaintext; otherwise fail

Equations

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

Oracle Record

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

Oracle interface for SAE games.

• sgen : Unit → Core.SPComp Unit
• senc : CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C
• sdec : CryptoTypes.C → CryptoTypes.Nonce → Core.SPComp (Option CryptoTypes.M)

SAE Game

noncomputable def CatCrypt.Examples.Cryptobox.SAE [CT : CryptoTypes] (E : NBSES) (b : Bool) (A : SAEOracles → Core.SPComp Bool) : Core.SPComp Bool

SAE game parameterized by real/ideal behavior b.

• b = false: real — encrypt/decrypt with actual key
• b = true: ideal — encrypt returns random ciphertext, decrypt checks log

Equations

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

SAE Advantage

noncomputable def CatCrypt.Examples.Cryptobox.saeAdvantage [CT : CryptoTypes] (E : NBSES) (A : SAEOracles → Core.SPComp Bool) : ENNReal

SAE advantage: distinguishing distance between real and ideal games.

Equations

• CatCrypt.Examples.Cryptobox.saeAdvantage E A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Cryptobox.SAE E false A) (CatCrypt.Examples.Cryptobox.SAE E true A)