ML-KEM: keygen/encaps/decaps and the KEM.KEM instance

keygen/encaps/decaps are FIPS 203 Algorithms 19-21, written against Primitives.primitives so that variants such as hedged encapsulation can change them locally.

Reliable s states that the draw from s decapsulates correctly. It is not characterized in terms of the sampled noise.

keygen / encaps / decaps

def Cryptlib.Primitives.KEM.FIPS203.keygen (ps : MLKEM.ParameterSet) (d z : MLKEM.Seed32) : MLKEM.EncapsulationKey (params ps) (encoding ps) × MLKEM.DecapsulationKey (params ps) (encoding ps)

ML-KEM.KeyGen_internal.

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.encaps (ps : MLKEM.ParameterSet) (ek : MLKEM.EncapsulationKey (params ps) (encoding ps)) (m : MLKEM.Message) : MLKEM.SharedSecret × MLKEM.Ciphertext (params ps) (encoding ps)

ML-KEM.Encaps_internal.

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decaps (ps : MLKEM.ParameterSet) (dk : MLKEM.DecapsulationKey (params ps) (encoding ps)) (c : MLKEM.Ciphertext (params ps) (encoding ps)) : MLKEM.SharedSecret

ML-KEM.Decaps_internal. Compares ciphertexts by their ByteArray encodings.

Equations

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

FIPS 203 §7.2/§7.3 input-validation checks

The internal algorithms above do not validate keys; callers run these checks first.

def Cryptlib.Primitives.KEM.FIPS203.checkEncapsulationKey (ps : MLKEM.ParameterSet) (ek : MLKEM.EncapsulationKey (params ps) (encoding ps)) : Bool

FIPS 203 §7.2 modulus check: tHatEncoded survives a decode/encode round trip.

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.checkDecapsulationKey (ps : MLKEM.ParameterSet) (dk : MLKEM.DecapsulationKey (params ps) (encoding ps)) : Bool

FIPS 203 §7.3 hash check: dk.ekHash = H(ekPKE).

Equations

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

keygen/encaps outputs are well-formed

theorem Cryptlib.Primitives.KEM.FIPS203.keygen_ek_wf (ps : MLKEM.ParameterSet) (d z : MLKEM.Seed32) : (tBytes ps (keygen ps d z).1.tHatEncoded).size = 384 * (params ps).k

theorem Cryptlib.Primitives.KEM.FIPS203.keygen_dk_wf (ps : MLKEM.ParameterSet) (d z : MLKEM.Seed32) : (tBytes ps (keygen ps d z).2.dkPKE.sHatEncoded).size = 384 * (params ps).k ∧ (tBytes ps (keygen ps d z).2.ekPKE.tHatEncoded).size = 384 * (params ps).k

State: a SHAKE-256 stream of 32-byte blocks from one 32-byte seed

def Cryptlib.Primitives.KEM.FIPS203.seedBlock (seed : Vector UInt8 32) (i : ℕ) : Vector UInt8 32

The i-th 32-byte block derived from seed.

Equations

• Cryptlib.Primitives.KEM.FIPS203.seedBlock seed i = Cryptlib.Util.Bytes.toVecN 32 (SLHDSA.Concrete.Keccak.shake256 ((Cryptlib.Util.Bytes.ofVector seed).push i.toUInt8) 32)

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.State : Type

Counter plus the original seed.

Equations

• Cryptlib.Primitives.KEM.FIPS203.State = (ℕ × Vector UInt8 32)

def Cryptlib.Primitives.KEM.FIPS203.nextDraw : EStateM KEM.KEMError State (Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.FIPS203.nextDraw (i, seed) = EStateM.Result.ok (Cryptlib.Primitives.KEM.FIPS203.seedBlock seed i) (i + 1, seed)

def Cryptlib.Primitives.KEM.FIPS203.stateFromSeed (seed : Vector UInt8 32) : State

Equations

• Cryptlib.Primitives.KEM.FIPS203.stateFromSeed seed = (0, seed)

The KEM.KEM instance

def Cryptlib.Primitives.KEM.FIPS203.Reliable (ps : MLKEM.ParameterSet) (s : State) : Prop

The next draw from s, encapsulated against any key pair, decapsulates correctly.

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.encapM (ps : MLKEM.ParameterSet) (pk : PublicKey ps) : EStateM KEM.KEMError State (CT ps × Vector UInt8 32)

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decapM (ps : MLKEM.ParameterSet) (sk : PrivateKey ps) (c : CT ps) : EStateM KEM.KEMError State (Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.FIPS203.decapM ps sk c = pure (Cryptlib.Primitives.KEM.FIPS203.decaps ps ↑sk ↑c)

def Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyM (ps : MLKEM.ParameterSet) (sk : PrivateKey ps) : PublicKey ps

Equations

• Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyM ps sk = ⟨(↑sk).ekPKE, ⋯⟩

theorem Cryptlib.Primitives.KEM.FIPS203.honestRoundTripM (ps : MLKEM.ParameterSet) (sk : PrivateKey ps) (s : State) (hrel : Reliable ps s) (c : CT ps) (k : Vector UInt8 32) (s' : State) (hc : encapM ps (derivePublicKeyM ps sk) s = EStateM.Result.ok (c, k) s') (t : State) : ∃ (t' : State), decapM ps sk c t = EStateM.Result.ok k t'

Round trip from a Reliable state. Uses simp only on hc; injection times out on the CT subtype.

theorem Cryptlib.Primitives.KEM.FIPS203.decodePrivateKey_totalM (ps : MLKEM.ParameterSet) (v : Vector UInt8 (params ps).secretKeyBytes) : ∃ (sk : PrivateKey ps), decodePrivateKey ps v = some sk

def Cryptlib.Primitives.KEM.FIPS203.dummySeed : MLKEM.Seed32

Equations

• Cryptlib.Primitives.KEM.FIPS203.dummySeed = Vector.replicate 32 0

def Cryptlib.Primitives.KEM.FIPS203.dummyPk (ps : MLKEM.ParameterSet) : PublicKey ps

Equations

• Cryptlib.Primitives.KEM.FIPS203.dummyPk ps = ⟨(Cryptlib.Primitives.KEM.FIPS203.keygen ps Cryptlib.Primitives.KEM.FIPS203.dummySeed Cryptlib.Primitives.KEM.FIPS203.dummySeed).1, ⋯⟩

def Cryptlib.Primitives.KEM.FIPS203.dummySk (ps : MLKEM.ParameterSet) : PrivateKey ps

Equations

• Cryptlib.Primitives.KEM.FIPS203.dummySk ps = ⟨(Cryptlib.Primitives.KEM.FIPS203.keygen ps Cryptlib.Primitives.KEM.FIPS203.dummySeed Cryptlib.Primitives.KEM.FIPS203.dummySeed).2, ⋯⟩

def Cryptlib.Primitives.KEM.FIPS203.dummyCt (ps : MLKEM.ParameterSet) : CT ps

Equations

• Cryptlib.Primitives.KEM.FIPS203.dummyCt ps = ⟨(Cryptlib.Primitives.KEM.FIPS203.encaps ps (↑(Cryptlib.Primitives.KEM.FIPS203.dummyPk ps)) Cryptlib.Primitives.KEM.FIPS203.dummySeed).2, ⋯⟩

def Cryptlib.Primitives.KEM.FIPS203.kem (ps : MLKEM.ParameterSet) : KEM.KEM

ML-KEM with the expanded FIPS 203 private key.

Equations

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

Seed-format private keys

kemSeed stores the private key as the seed (d, z), encoded ek ‖ d ‖ z, and re-expands it on use. Everything else is as in kem.

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.SeedPrivateKey : Type

Equations

• Cryptlib.Primitives.KEM.FIPS203.SeedPrivateKey = (MLKEM.Seed32 × MLKEM.Seed32)

def Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyFromSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) : PublicKey ps

Equations

• Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyFromSeed ps sk = ⟨(Cryptlib.Primitives.KEM.FIPS203.keygen ps sk.1 sk.2).1, ⋯⟩

def Cryptlib.Primitives.KEM.FIPS203.expandSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) : PrivateKey ps

The expanded decapsulation key for a seed, recomputed on every call.

Equations

• Cryptlib.Primitives.KEM.FIPS203.expandSeed ps sk = ⟨(Cryptlib.Primitives.KEM.FIPS203.keygen ps sk.1 sk.2).2, ⋯⟩

def Cryptlib.Primitives.KEM.FIPS203.decapMFromSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) (c : CT ps) : EStateM KEM.KEMError State (Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.FIPS203.decapMFromSeed ps sk c = Cryptlib.Primitives.KEM.FIPS203.decapM ps (Cryptlib.Primitives.KEM.FIPS203.expandSeed ps sk) c

theorem Cryptlib.Primitives.KEM.FIPS203.honestRoundTripFromSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) (s : State) : Reliable ps s → ∀ (c : CT ps) (k : Vector UInt8 32) (s' : State), encapM ps (derivePublicKeyFromSeed ps sk) s = EStateM.Result.ok (c, k) s' → ∀ (t : State), ∃ (t' : State), decapMFromSeed ps sk c t = EStateM.Result.ok k t'

def Cryptlib.Primitives.KEM.FIPS203.encodePrivateKeyFromSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) : Vector UInt8 ((params ps).publicKeyBytes + 64)

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decodePrivateKeyFromSeed (ps : MLKEM.ParameterSet) (v : Vector UInt8 ((params ps).publicKeyBytes + 64)) : Option SeedPrivateKey

Equations

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

theorem Cryptlib.Primitives.KEM.FIPS203.decodePrivateKeyFromSeed_total (ps : MLKEM.ParameterSet) (v : Vector UInt8 ((params ps).publicKeyBytes + 64)) : ∃ (sk : SeedPrivateKey), decodePrivateKeyFromSeed ps v = some sk

theorem Cryptlib.Primitives.KEM.FIPS203.decode_encode_privFromSeed (ps : MLKEM.ParameterSet) (sk : SeedPrivateKey) : decodePrivateKeyFromSeed ps (encodePrivateKeyFromSeed ps sk) = some sk

def Cryptlib.Primitives.KEM.FIPS203.kemSeed (ps : MLKEM.ParameterSet) : KEM.KEM

ML-KEM with the ek ‖ d ‖ z seed private key.

Equations

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