HKDF: HMAC-based Key Derivation Function (RFC 5869)

Extract maps (salt, IKM) to a digest-sized PRK; Expand maps (PRK, info, len) to exactly len bytes.

structure Cryptlib.Primitives.Hash.HKDF.HKDF : Type 1

• hash : Hash.Hash
• PRK : Type
• encodePRK : self.PRK → Vector UInt8 self.hash.digestSize
• decodePRK : Vector UInt8 self.hash.digestSize → Option self.PRK
• extract : ByteArray → ByteArray → self.PRK
• expand : self.PRK → ByteArray → (len : Nat) → Vector UInt8 len
• decode_encode_prk (prk : self.PRK) : self.decodePRK (self.encodePRK prk) = some prk
• expand_size (prk : self.PRK) (info : ByteArray) (len : Nat) : (self.expand prk info len).toArray.size = len

def Cryptlib.Primitives.Hash.HKDF.trivialHKDF : HKDF

Equations

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

@[instance_reducible]

instance Cryptlib.Primitives.Hash.HKDF.instInhabitedHKDF : Inhabited HKDF

Equations

• Cryptlib.Primitives.Hash.HKDF.instInhabitedHKDF = { default := Cryptlib.Primitives.Hash.HKDF.trivialHKDF }

HKDF-BLAKE2b-512

@[reducible]

def Cryptlib.Primitives.Hash.HKDF.blake2b_hashScheme : Hash.Hash

BLAKE2b-512 as a Hash: accumulate the message, hash at finalize.

Equations

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

def Cryptlib.Primitives.Hash.HKDF.ofHash (H : Hash.Hash) : HKDF

Extract-then-Expand over any Hash, the PRK being one digest.

Equations

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

def Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf : HKDF

Equations

• Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf = Cryptlib.Primitives.Hash.HKDF.ofHash Cryptlib.Primitives.Hash.HKDF.blake2b_hashScheme