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).
8	import Base
9	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10	import ./crypto.bend as Cr
11	import ./hmac.bend as Hm
12	
13	def 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
21	def 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)
25	def 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	
33	def 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	
40	def 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	
49	def 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
57	def 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)
61	def 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)