Key-derivation functions

Expand-only: the input keying material is used directly, with no Extract step.

structure Cryptlib.Primitives.KDF.KDF : Type

• expand : ByteArray → ByteArray → (len : Nat) → ByteArray

  Expand (ikm, info) into exactly len bytes of output key material.

• expand_size (ikm info : ByteArray) (len : Nat) : (self.expand ikm info len).size = len

@[instance_reducible]

instance Cryptlib.Primitives.KDF.instInhabitedKDF : Inhabited KDF

The empty KDF, to show KDF is inhabited. Not a KDF.

Equations

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