~/bend-docscommunity

spec/crypto/hkdf.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/hkdf.bend as Hkdf

2 imports
import Base
import ./hmac.bend as HMAC

Definitions

def hash_len source · line 8 · raw

Nat

def max_length source · line 12 · raw

Nat

RFC 5869: L <= 255*HashLen.

def extract source · line 18 · raw

@+salt:List<&2, U32> -> @ikm:List<&2, U32> -> List<&2, U32>

2.2 Step 1: Extract. PRK = HMAC-Hash(salt, IKM). An absent salt is HashLen zero bytes; an empty salt gives the same HMAC key block (both are padded with zeros to the block size), so passing [] means "not provided".

def t_blocks source · line 24 · raw

@n:Nat -> @+prk:List<&2, U32> -> @+info:List<&2, U32> -> @prev:List<&2, U32> -> @+i:Nat -> List<&2, U32>

2.3 Step 2: Expand. T(0) = empty string; for i = 1..N, T(i) = HMAC-Hash(PRK, T(i-1) | info | the octet i). t_blocks(n, prk, info, T(i), i) is T(i+1) | ... | T(i+n).

def block_count source · line 34 · raw

@+len:Nat -> Nat

N = ceil(L/HashLen).

def okm source · line 38 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> List<&2, U32>

OKM = the first L octets of T = T(1) | T(2) | ... | T(N).

def expand_if source · line 42 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> @ok:Bool -> Maybe<&2, List<&2, U32>>

Expand is defined for L <= 255*HashLen only.

def expand source · line 49 · raw

@+prk:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> Maybe<&2, List<&2, U32>>

def hkdf source · line 52 · raw

@+salt:List<&2, U32> -> @ikm:List<&2, U32> -> @+info:List<&2, U32> -> @+len:Nat -> Maybe<&2, List<&2, U32>>