Sphinx packet key derivation

HKDF-Expand of the shared secret into 160 bytes, sliced into five keys.

def Cryptlib.Protocols.Sphinx.KDF.kdfInfo : ByteArray

Equations

• Cryptlib.Protocols.Sphinx.KDF.kdfInfo = { data := "katzenpost-kdf-v0-hkdf-sha256".toUTF8.data }

structure Cryptlib.Protocols.Sphinx.KDF.PacketKeys : Type

The per-hop packet keys, in OKM order.

• headerMAC : Vector UInt8 32
• headerEncryption : Vector UInt8 32
• headerEncryptionIV : Vector UInt8 16
• payloadEncryption : Vector UInt8 48
• blindingFactorSeed : Vector UInt8 32

def Cryptlib.Protocols.Sphinx.KDF.sliceV (b : ByteArray) (off len : Nat) : Vector UInt8 len

A len-byte slice of b as a fixed-width vector.

Equations

• Cryptlib.Protocols.Sphinx.KDF.sliceV b off len = Vector.ofFn fun (i : Fin len) => b.data.getD (off + ↑i) 0

def Cryptlib.Protocols.Sphinx.KDF.sphinxKDF (ikm : ByteArray) : PacketKeys

Derive PacketKeys from a shared secret with HKDF-SHA256.

Equations

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

def Cryptlib.Protocols.Sphinx.KDF.packetKeysFrom (kdf : Primitives.KDF.KDF) (ikm : ByteArray) : PacketKeys

Derive PacketKeys with an arbitrary KDF.

Equations

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

theorem Cryptlib.Protocols.Sphinx.KDF.packetKeysFrom_hkdfSha256Expand (ikm : ByteArray) : packetKeysFrom Primitives.KDF.HKDF.hkdfSha256Expand ikm = sphinxKDF ikm

packetKeysFrom hkdfSha256Expand is sphinxKDF.