src/crypto/kdf.bend

bend-collections@1.0.0.0 · 50 lines · 7 definitions

1import Base
2import bend-collections@1.0.0.0/src/crypto/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
17type KdfError is Data:
18  LengthTooLarge{}
19
20def max_length() -> Nat:
21  8160n
22
23def 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.
29def 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
39def 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
46def 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
49def 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)