HKDF (RFC 5869), over any Hash

def Cryptlib.Primitives.KDF.HKDF.extract (H : Hash.Hash.Hash) (salt ikm : ByteArray) : Vector UInt8 H.digestSize

RFC 5869 §2.2 Extract. An empty salt stands for digestSize zero bytes.

Equations

• Cryptlib.Primitives.KDF.HKDF.extract H salt ikm = Cryptlib.Primitives.MAC.HMAC.hmac H (if salt.size = 0 then { data := Array.replicate H.digestSize 0 } else salt) ikm

def Cryptlib.Primitives.KDF.HKDF.expand (H : Hash.Hash.Hash) (prk info : ByteArray) (len : Nat) : ByteArray

RFC 5869 §2.3 Expand: iterated HMAC over (PRK, T(i-1) ‖ info ‖ i), truncated to len.

Equations

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

def Cryptlib.Primitives.KDF.HKDF.expand.go (H : Hash.Hash.Hash) (prk info : ByteArray) : Nat → Nat → ByteArray → ByteArray → ByteArray

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.KDF.HKDF.expand.go H prk info 0 a✝² a✝¹ a✝ = a✝

theorem Cryptlib.Primitives.KDF.HKDF.expand_size (H : Hash.Hash.Hash) (prk info : ByteArray) (len : Nat) : (expand H prk info len).size = len

def Cryptlib.Primitives.KDF.HKDF.kdfOf (H : Hash.Hash.Hash) : KDF

Expand-only HKDF as a KDF, the raw input keying material used directly as the PRK.

Equations

• Cryptlib.Primitives.KDF.HKDF.kdfOf H = { expand := Cryptlib.Primitives.KDF.HKDF.expand H, expand_size := ⋯ }

def Cryptlib.Primitives.KDF.HKDF.hkdfSha256Expand : KDF

Equations

• Cryptlib.Primitives.KDF.HKDF.hkdfSha256Expand = Cryptlib.Primitives.KDF.HKDF.kdfOf Cryptlib.Primitives.Hash.Sha2.Sha256.Scheme