spec/crypto/hkdf.bend

bend-collections@1.0.0.0 · 53 lines · 9 definitions

1import Base
2import bend-collections@1.0.0.0/spec/crypto/hmac.bend as HMAC
3
4# Executable specification of HKDF-SHA256, RFC 5869 section 2, over the
5# HMAC specification spec/crypto/hmac.bend (after HACL*'s Spec.HKDF).
6# Nothing of the implementation (src/crypto/kdf.bend) is used.
7
8def hash_len() -> Nat:
9  32n
10
11# RFC 5869: L <= 255*HashLen.
12def max_length() -> Nat:
13  8160n
14
15# 2.2 Step 1: Extract. PRK = HMAC-Hash(salt, IKM). An absent salt is HashLen
16# zero bytes; an empty salt gives the same HMAC key block (both are padded
17# with zeros to the block size), so passing [] means "not provided".
18def extract(+salt: List<&2, U32>, ikm: List<&2, U32>) -> List<&2, U32>:
19  HMAC.hmac(salt, ikm)
20
21# 2.3 Step 2: Expand. T(0) = empty string; for i = 1..N,
22#   T(i) = HMAC-Hash(PRK, T(i-1) | info | the octet i).
23# t_blocks(n, prk, info, T(i), i) is T(i+1) | ... | T(i+n).
24def t_blocks(n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, prev: List<&2, U32>, +i: Nat) -> List<&2, U32>:
25  match n:
26    case 0n:
27      Nil{}
28    case 1n+p:
29      +t = HMAC.hmac(prk, List.append(&2, U32, prev,
30        List.append(&2, U32, info, [U32.from_nat(1n+i)])))
31      List.append(&2, U32, t, t_blocks(p, prk, info, t, 1n+i))
32
33# N = ceil(L/HashLen).
34def block_count(+len: Nat) -> Nat:
35  Nat.div(Nat.add(len, 31n), hash_len())
36
37# OKM = the first L octets of T = T(1) | T(2) | ... | T(N).
38def okm(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> List<&2, U32>:
39  List.take(&2, U32, t_blocks(block_count(len), prk, info, Nil{}, 0n), len)
40
41# Expand is defined for L <= 255*HashLen only.
42def expand_if(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
43  match ok:
44    case True{}:
45      Some{okm(prk, info, len)}
46    case False{}:
47      None{}
48
49def expand(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Maybe<&2, List<&2, U32>>:
50  expand_if(prk, info, len, Nat.is_le(len, max_length()))
51
52def hkdf(+salt: List<&2, U32>, ikm: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Maybe<&2, List<&2, U32>>:
53  expand(extract(salt, ikm), info, len)