1	import Base
2	import ./mac.bend as MAC
3	
4	# HKDF-SHA256 (RFC 5869), on HMAC-SHA256 (src/crypto/mac.bend).
5	#
6	#   extract(salt, ikm) -> prk                 32-byte pseudorandom key
7	#   expand(prk, info, len) -> Done{okm} | Fail{LengthTooLarge{}}
8	#   hkdf(salt, ikm, info, len)                expand(extract(salt, ikm), info, len)
9	#
10	# len is at most 255 * 32 = 8160 bytes; a larger len is the error value
11	# LengthTooLarge (never a crash). An empty salt means "no salt" (RFC 5869:
12	# HashLen zero bytes, which gives the same HMAC key). The specification is
13	# spec/crypto/hkdf.bend; proofs/crypto/kdf/proof.bend proves expand equal to
14	# it for every input, the output length, and that a shorter output is a
15	# prefix of a longer one.
16	
17	type KdfError is Data:
18	  LengthTooLarge{}
19	
20	def max_length() -> Nat:
21	  8160n
22	
23	def extract(+salt: List<&2, U32>, ikm: List<&2, U32>) -> List<&2, U32>:
24	  MAC.sign(salt, ikm)
25	
26	# The blocks T(i), T(i+1), ... cut to rem bytes: prev is T(i-1) and ctr the
27	# counter byte i. Generation stops as soon as rem bytes are out, and no
28	# block count is computed.
29	def blocks(rem: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, prev: List<&2, U32>, +ctr: U32) -> List<&2, U32>:
30	  match rem:
31	    case 0n:
32	      Nil{}
33	    case 32n+r:
34	      +t = MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [ctr])))
35	      List.append(&2, U32, t, blocks(r, prk, info, t, U32.inc(ctr)))
36	    case 1n+p:
37	      List.take(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [ctr]))), 1n+p)
38	
39	def expand_if(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, ok: Bool) -> Result<&2, &2, KdfError, List<&2, U32>>:
40	  match ok:
41	    case True{}:
42	      Done{blocks(len, prk, info, Nil{}, 1)}
43	    case False{}:
44	      Fail{LengthTooLarge{}}
45	
46	def expand(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Result<&2, &2, KdfError, List<&2, U32>>:
47	  expand_if(prk, info, len, Nat.is_le(len, max_length()))
48	
49	def hkdf(+salt: List<&2, U32>, ikm: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Result<&2, &2, KdfError, List<&2, U32>>:
50	  expand(extract(salt, ikm), info, len)