hkdf.bend

bend-osdev-crypto@0.1.0.0 · 62 lines · 8 definitions

1# HKDF over any hash (RFC 5869), on HMAC (hmac.bend):
2#   PRK = HMAC(salt, IKM), the salt dsize zero bytes when it is empty
3#   T(0) = empty, T(i) = HMAC(PRK, T(i-1) || info || i), i = 1 .. N
4#   OKM = the first len bytes of T(1) || T(2) || ... || T(N), N = ceil(len/dsize)
5# len is at most 255 dsize (CrBadOutputLength otherwise). As a KDF
6# (kdf.bend), HKDF over a hash (~bsize, ~dsize, ~digest, from its
7# interface) is the instance ~CrHkdf.derive(~bsize, ~dsize, ~digest).
8import Base
9import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
11import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
12
13def cr.hkdf.salt(empty: Bool, +n: Nat, +salt: B.Octets) -> B.Octets:
14  match empty:
15    case True{}:
16      B.Octets.zeros(n)
17    case False{}:
18      salt
19
20# Extract: the pseudorandom key of the input keying material ikm
21def CrHkdf.extract(~bsize: Nat, ~dsize: Nat, ~digest: B.Octets -> B.Octets, +salt: B.Octets, ikm: B.Octets) -> B.Octets:
22  Hm.CrHmac.mac(~digest, Hm.CrHmac.key(~bsize, ~digest, cr.hkdf.salt(Nat.is_eq(B.Octets.len(salt), 0n), dsize, salt)), ikm)
23
24# T(i) .. T(i+n-1), last first, onto acc (prev is T(i-1), ctr the byte i)
25def cr.hkdf.blocks(~digest: B.Octets -> B.Octets, n: Nat, +kk: Hm.CrHmacKey, +info: B.Octets, prev: B.Octets, +ctr: U32, acc: List<&2, B.Octets>) -> List<&2, B.Octets>:
26  match n:
27    case 0n:
28      acc
29    case 1n+p:
30      +t = Hm.CrHmac.mac(~digest, kk, B.Octets.append(prev, B.Octets.append(info, B.Octets.of_list([ctr]))))
31      cr.hkdf.blocks(~digest, p, kk, info, t, U32.add(ctr, 1), Con{t, acc})
32
33def cr.hkdf.rev(os: List<&2, B.Octets>, acc: List<&2, B.Octets>) -> List<&2, B.Octets>:
34  match os:
35    case Nil{}:
36      acc
37    case Con{h, t}:
38      cr.hkdf.rev(t, Con{h, acc})
39
40def cr.hkdf.expand(~bsize: Nat, ~dsize: Nat, ~digest: B.Octets -> B.Octets, ok: Bool, +prk: B.Octets, +info: B.Octets, +len: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
41  match ok:
42    case False{}:
43      Fail{Cr.CrBadOutputLength{len}}
44    case True{}:
45      +n = Nat.div(Nat.add(len, Nat.sub(dsize, 1n)), dsize)
46      +ts = cr.hkdf.blocks(~digest, n, Hm.CrHmac.key(~bsize, ~digest, prk), info, B.Octets.empty(), 1, Nil{})
47      Done{B.Octets.take(len, B.Octets.concat(cr.hkdf.rev(ts, Nil{})))}
48
49def cr.hkdf.ok(pos: Bool, +len: Nat, +dsize: Nat) -> Bool:
50  match pos:
51    case True{}:
52      Nat.is_le(len, Nat.mul(255n, dsize))
53    case False{}:
54      False{}
55
56# Expand: len bytes of output keying material from the pseudorandom key
57def CrHkdf.expand(~bsize: Nat, ~dsize: Nat, ~digest: B.Octets -> B.Octets, +prk: B.Octets, +info: B.Octets, +len: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
58  cr.hkdf.expand(~bsize, ~dsize, ~digest, cr.hkdf.ok(Nat.is_lt(0n, dsize), len, dsize), prk, info, len)
59
60# Extract, then expand: the KDF interface's ~derive (secret, salt, info, len)
61def CrHkdf.derive(~bsize: Nat, ~dsize: Nat, ~digest: B.Octets -> B.Octets, ikm: B.Octets, salt: B.Octets, info: B.Octets, len: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
62  CrHkdf.expand(~bsize, ~dsize, ~digest, CrHkdf.extract(~bsize, ~dsize, ~digest, salt, ikm), info, len)