def Cryptlib.Primitives.KEM.sha256V (b : ByteArray) : Vector UInt8 32

SHA-256, retyped to Vector UInt8 32.

Equations

• Cryptlib.Primitives.KEM.sha256V b = Vector.mk (↑(Cryptlib.Primitives.Hash.Sha2.Sha256.hash b)).data ⋯

def Cryptlib.Primitives.KEM.u32be (n : ℕ) : ByteArray

Big-endian u32.

Equations

• Cryptlib.Primitives.KEM.u32be n = { data := #[(n >>> 24).toUInt8, (n >>> 16).toUInt8, (n >>> 8).toUInt8, n.toUInt8] }

def Cryptlib.Primitives.KEM.lenPrefixed (b : ByteArray) : ByteArray

A field under a big-endian 32-bit length prefix.

Equations

• Cryptlib.Primitives.KEM.lenPrefixed b = Cryptlib.Primitives.KEM.u32be b.size ++ b

def Cryptlib.Primitives.KEM.sha256v1Label : ByteArray

Domain-separation tag for sha256-v1.

Equations

• Cryptlib.Primitives.KEM.sha256v1Label = "kemadapter-sha256-v1".toUTF8

def Cryptlib.Primitives.KEM.sha256v1Derive (ss pkStatic pkEph : ByteArray) (outLen : ℕ) : Vector UInt8 outLen

The sha256-v1 PRF:

SHA256(label || u32be(len(ss))       || ss
             || u32be(len(pkStatic)) || pkStatic
             || u32be(len(pkEph))    || pkEph)

Only meaningful at outLen = 32; other widths are zero-padded or truncated.

Equations

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

def Cryptlib.Primitives.KEM.sha256v1PRF : Adapter.PRF

Equations

• Cryptlib.Primitives.KEM.sha256v1PRF = { name := "sha256-v1", derive := Cryptlib.Primitives.KEM.sha256v1Derive }

def Cryptlib.Primitives.KEM.blake2bXOFDerive (ss pkStatic pkEph : ByteArray) (outLen : ℕ) : Vector UInt8 outLen

The blake2b-xof PRF: a BLAKE2b XOF keyed by ss, or by BLAKE2b-256 of ss if it is not 32 bytes.

Equations

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

def Cryptlib.Primitives.KEM.blake2bXOFPRF : Adapter.PRF

Equations

• Cryptlib.Primitives.KEM.blake2bXOFPRF = { name := "blake2b-xof", derive := Cryptlib.Primitives.KEM.blake2bXOFDerive }

def Cryptlib.Primitives.KEM.kemX25519Ladder : KEM.KEM

X25519 (Montgomery ladder) as a KEM.

Equations

• Cryptlib.Primitives.KEM.kemX25519Ladder = Cryptlib.Primitives.KEM.Adapter.kemOfNike Cryptlib.Primitives.KEM.sha256v1PRF Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.LadderScheme

def Cryptlib.Primitives.KEM.kemX25519 : KEM.KEM

X25519 (limb ladder) as a KEM.

Equations

• Cryptlib.Primitives.KEM.kemX25519 = Cryptlib.Primitives.KEM.Adapter.kemOfNike Cryptlib.Primitives.KEM.sha256v1PRF Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.FeScheme

def Cryptlib.Primitives.KEM.kemX25519Blake2b : KEM.KEM

X25519 as a KEM with the blake2b-xof PRF. Not registered.

Equations

• Cryptlib.Primitives.KEM.kemX25519Blake2b = Cryptlib.Primitives.KEM.Adapter.kemOfNike Cryptlib.Primitives.KEM.blake2bXOFPRF Cryptlib.Primitives.NIKE.X25519.Scheme

The KEM registry

Names use only [A-Za-z0-9/], as in Noise protocol names. X25519 KEMs carry a KEM suffix to stay distinct from the X25519 NIKEs. ML-KEM private keys are in the seed form ek ‖ d ‖ z.

structure Cryptlib.Primitives.KEM.RegistryEntry : Type 1

• name : String
• scheme : KEM.KEM

def Cryptlib.Primitives.KEM.blake2b256CombinerPRF : Combiner.PRF

Combiner.PRF with unkeyed and keyed BLAKE2b-256.

Equations

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

def Cryptlib.Primitives.KEM.withX25519 (pq : KEM.KEM) : KEM.KEM

X25519 combined with a post-quantum KEM via the split-PRF combiner (not X-Wing). IND-CCA2 if either component is (https://eprint.iacr.org/2018/024.pdf, Theorem 1).

Equations

• Cryptlib.Primitives.KEM.withX25519 pq = Cryptlib.Primitives.KEM.Combiner.combineKEM Cryptlib.Primitives.KEM.blake2b256CombinerPRF Cryptlib.Primitives.KEM.kemX25519 [pq]

def Cryptlib.Primitives.KEM.kemMLKEM512X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEM512X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEM512.kemMLKEM512Seed

def Cryptlib.Primitives.KEM.kemMLKEM768X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEM768X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEM768.kemMLKEM768Seed

def Cryptlib.Primitives.KEM.kemMLKEM1024X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEM1024X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEM1024.kemMLKEM1024Seed

def Cryptlib.Primitives.KEM.kemMLKEMHedged512X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEMHedged512X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged512Seed

def Cryptlib.Primitives.KEM.kemMLKEMHedged768X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEMHedged768X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged768Seed

def Cryptlib.Primitives.KEM.kemMLKEMHedged1024X25519 : KEM.KEM

Equations

• Cryptlib.Primitives.KEM.kemMLKEMHedged1024X25519 = Cryptlib.Primitives.KEM.withX25519 Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged1024Seed

def Cryptlib.Primitives.KEM.kemMLKEM768X25519Blake2b : KEM.KEM

kemMLKEM768X25519 over kemX25519Blake2b. Not registered.

Equations

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

def Cryptlib.Primitives.KEM.registry : List RegistryEntry

Every registered KEM. The hedged schemes restore round-3 Kyber's m ← H(m) and are not FIPS 203.

Equations

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

def Cryptlib.Primitives.KEM.byName (name : String) : Option KEM.KEM

Case-insensitive lookup by registry name.

Equations

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