Cryptobox Scheme Definitions

Abstract type definitions and scheme records for NaCl's Cryptobox construction. Cryptobox 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).

Main definitions

• NBSES — Nonce-based symmetric encryption scheme (enc/dec with shared key + nonce)
• NIKEScheme — Non-interactive key exchange (pkgen + deterministic shared key derivation)
• KeyInjection — Injection between NIKE and NBSES key spaces
• SID — Session identifier (canonical pair of public keys)
• sortSID — Canonical ordering for session IDs

Design choices

Following the Rocq SSProve Cryptobox (nominal-ssprove), all key types (PK, SK, SharedKey) are Fintype to enable uniform sampling. Messages and ciphertexts are also Fintype for simplicity (the Rocq version uses choice_type which allows infinite types, but Lean's SPComp.sample requires Fintype).

All scheme operations are pure SPComp computations (no state). State is introduced only in the game definitions (PKEY, KEY, SAE, etc.).

References

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

Abstract types

These are parameters throughout the Cryptobox formalization. Each file will declare the necessary variables.

class CatCrypt.Examples.Cryptobox.CryptoTypes : Type 1

Abstract type bundle for Cryptobox. All types are finite (for uniform sampling) and have decidable equality (for map lookups and equality checks in games).

• PK : Type
• SK : Type
• SharedKey : Type
• Nonce : Type
• M : Type
• C : Type
• finPK : Fintype PK
• finSK : Fintype SK
• finSharedKey : Fintype SharedKey
• finNonce : Fintype Nonce
• finM : Fintype M
• finC : Fintype C
• inhPK : Inhabited PK
• inhSK : Inhabited SK
• inhSharedKey : Inhabited SharedKey
• inhNonce : Inhabited Nonce
• inhM : Inhabited M
• inhC : Inhabited C
• decPK : DecidableEq PK
• decSK : DecidableEq SK
• decSharedKey : DecidableEq SharedKey
• decNonce : DecidableEq Nonce
• decM : DecidableEq M
• decC : DecidableEq C

Nonce-Based Symmetric Encryption Scheme (NBSES)

Corresponds to Rocq's NBSES_scheme. In NaCl, this is XSalsa20-Poly1305. All operations are pure SPComp (no state, no oracle access).

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

Nonce-Based Symmetric Encryption Scheme. Parameterized by a CryptoTypes instance providing the abstract types.

• enc : CryptoTypes.SharedKey → CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C

  Probabilistic encryption: key → message → nonce → ciphertext

• dec : CryptoTypes.SharedKey → CryptoTypes.C → CryptoTypes.Nonce → Core.SPComp (Option CryptoTypes.M)

  Decryption: key → ciphertext → nonce → message (may fail for AEAD)

Non-Interactive Key Exchange (NIKE)

Corresponds to Rocq's NIKE_scheme. In NaCl, this is X25519. The shared key computation is deterministic (pure function).

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

Non-Interactive Key Exchange scheme.

• pkgen : Core.SPComp (CryptoTypes.PK × CryptoTypes.SK)

  Key pair generation (probabilistic)

• sharedkey : CryptoTypes.PK → CryptoTypes.SK → CryptoTypes.SharedKey

  Shared key derivation (deterministic). Given a remote public key and local secret key, computes a shared secret. In NaCl: X25519(sk, pk).

Key Injection

Corresponds to Rocq's inj record. Maps between NIKE shared keys and NBSES shared keys. In practice, this is often the identity or a hash.

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

Injection between key spaces (NIKE shared keys ↔ NBSES shared keys). Allows composing NIKE and NBSES even if their key types differ abstractly.

• encode : CryptoTypes.SharedKey → CryptoTypes.SharedKey

  Encode a NIKE shared key for use as an NBSES key

• decode : CryptoTypes.SharedKey → CryptoTypes.SharedKey

  Decode back

• cancels (k : CryptoTypes.SharedKey) : self.decode (self.encode k) = k

  Round-trip: decode ∘ encode = id

Session Identifiers (SID)

A session ID is a canonical pair of public keys identifying a communication session between two parties. The canonical ordering ensures both parties compute the same SID regardless of who is sender/receiver.

@[reducible, inline]

abbrev CatCrypt.Examples.Cryptobox.SID [CT : CryptoTypes] : Type

Session identifier: a pair of public keys.

Equations

• CatCrypt.Examples.Cryptobox.SID = (CatCrypt.Examples.Cryptobox.CryptoTypes.PK × CatCrypt.Examples.Cryptobox.CryptoTypes.PK)

noncomputable def CatCrypt.Examples.Cryptobox.sortSID [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (pk1 pk2 : CryptoTypes.PK) : SID

Canonical sort for session IDs. Ensures sortSID pk_a pk_b = sortSID pk_b pk_a.

Equations

• CatCrypt.Examples.Cryptobox.sortSID pk1 pk2 = if pk1 ≤ pk2 then (pk1, pk2) else (pk2, pk1)

theorem CatCrypt.Examples.Cryptobox.sortSID_comm [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (pk1 pk2 : CryptoTypes.PK) : sortSID pk1 pk2 = sortSID pk2 pk1

sortSID is symmetric: the order of arguments doesn't matter.

NIKE Commutativity

The key property for Cryptobox: the shared key is the same regardless of which party acts as sender/receiver. This is stated as a property of (NIKEScheme, pkgen output) pairs rather than as a field of NIKEScheme, following the Rocq approach.

def CatCrypt.Examples.Cryptobox.NIKEScheme.Commutative [CT : CryptoTypes] (N : NIKEScheme) : Prop

NIKE commutativity: shared key is the same regardless of role. For honestly generated key pairs (pk_a, sk_a) and (pk_b, sk_b): sharedkey pk_a sk_b = sharedkey pk_b sk_a

Equations

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

Nonce-Based Public-key Encryption Scheme (NBPES/PKAE)

The target construction: public-key authenticated encryption. Corresponds to Rocq's NBPES_scheme.

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

Nonce-Based Public-key Encryption Scheme (PKAE target).

• pkgen : Core.SPComp (CryptoTypes.PK × CryptoTypes.SK)

  Key pair generation

• enc : CryptoTypes.SK → CryptoTypes.PK → CryptoTypes.M → CryptoTypes.Nonce → Core.SPComp CryptoTypes.C

  Encryption: sender's SK, receiver's PK, message, nonce → ciphertext

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

  Decryption: receiver's SK, sender's PK, ciphertext, nonce → message

Cryptobox Construction

The main construction: combine NIKE + NBSES into a PKAE scheme.

noncomputable def CatCrypt.Examples.Cryptobox.cryptobox [CT : CryptoTypes] (N : NIKEScheme) (E : NBSES) (I : KeyInjection) : NBPES

Construct a PKAE scheme from NIKE + NBSES + key injection. This is the Cryptobox construction:

• pkgen = NIKE.pkgen
• enc(sk_s, pk_r, m, n) = NBSES.enc(inj(NIKE.sharedkey(pk_r, sk_s)), m, n)
• dec(sk_r, pk_s, c, n) = NBSES.dec(inj(NIKE.sharedkey(pk_s, sk_r)), c, n)

Equations

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

Operation identifiers

Fixed natural number identifiers for each oracle operation. These correspond to the Rocq operation IDs and are used for interface matching in the package system.

def CatCrypt.Examples.Cryptobox.opGEN : ℕ

Operation ID for key generation

Equations

• CatCrypt.Examples.Cryptobox.opGEN = 2

def CatCrypt.Examples.Cryptobox.opCSETPK : ℕ

Operation ID for corrupt set public key

Equations

• CatCrypt.Examples.Cryptobox.opCSETPK = 3

def CatCrypt.Examples.Cryptobox.opGETSK : ℕ

Operation ID for get secret key

Equations

• CatCrypt.Examples.Cryptobox.opGETSK = 4

def CatCrypt.Examples.Cryptobox.opHONPK : ℕ

Operation ID for check honest public key

Equations

• CatCrypt.Examples.Cryptobox.opHONPK = 5

def CatCrypt.Examples.Cryptobox.opSHAREDKEY : ℕ

Operation ID for NIKE shared key computation

Equations

• CatCrypt.Examples.Cryptobox.opSHAREDKEY = 24

def CatCrypt.Examples.Cryptobox.opSET : ℕ

Operation ID for honest key set

Equations

• CatCrypt.Examples.Cryptobox.opSET = 27

def CatCrypt.Examples.Cryptobox.opCSET : ℕ

Operation ID for corrupt key set

Equations

• CatCrypt.Examples.Cryptobox.opCSET = 28

def CatCrypt.Examples.Cryptobox.opGET : ℕ

Operation ID for key get

Equations

• CatCrypt.Examples.Cryptobox.opGET = 29

def CatCrypt.Examples.Cryptobox.opHON : ℕ

Operation ID for honesty check

Equations

• CatCrypt.Examples.Cryptobox.opHON = 30

def CatCrypt.Examples.Cryptobox.opENC : ℕ

Operation ID for encryption

Equations

• CatCrypt.Examples.Cryptobox.opENC = 31

def CatCrypt.Examples.Cryptobox.opDEC : ℕ

Operation ID for decryption

Equations

• CatCrypt.Examples.Cryptobox.opDEC = 32