pbkdf2.bend

bend-osdev-crypto@0.1.0.0 · 118 lines · 12 definitions

1# PBKDF2 over any MAC (RFC 8018, PKCS #5 v2.1, section 5.2), on the MAC
2# interface (mac.bend) as its pseudorandom function PRF:
3#   DK = T_1 || T_2 || ... , cut to dkLen bytes,
4#   T_i = F(P, S, c, i) = U_1 xor U_2 xor ... xor U_c,
5#   U_1 = PRF(P, S || INT(i)), U_j = PRF(P, U_(j-1)),
6# INT(i) the four-byte big-endian block index, from 1. The PRF's key is the
7# password P; a MAC that refuses P's length refuses the derivation (its own
8# CrError). In practice the PRF is HMAC over a hash (hmac.bend); any MAC
9# with hLen-byte tags will do.
10#
11# Refused (RFC 8018 step 1, and the iteration count's lower bound): an
12# iteration count c of 0 (CrTooShort{0}: too few iterations), an output
13# longer than (2^32 - 1) hLen bytes, or any output when hLen is 0
14# (CrBadOutputLength{dkLen}).
15#
16# The output is generated a byte at a time, each T_i computed when the
17# bytes before it are used up, so its length is dkLen for every MAC and
18# input (LAWS.bend: pbkdf2_length), and a shorter output is a prefix of a
19# longer one (pbkdf2_stream_prefix). As a KDF (kdf.bend), PBKDF2 over a MAC
20# (~K, ~key, ~compute, and its tag length ~hlen) with c iterations is
21#   ~CrPbkdf2.derive(~K, ~key, ~compute, ~hlen, ~c)
22# whose context argument (info) is unused: PBKDF2 has none. The named
23# instances (PBKDF2-HMAC-SHA-256 and PBKDF2-HMAC-SHA-1) are in
24# inst_pbkdf2.bend.
25import Base
26import bend-osdev-bytes@0.1.0.0/bytes.bend as B
27import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
28
29# bytewise XOR of two tags (as long as the shorter)
30def cr.pbkdf2.xor(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
31  match xs ys:
32    case Con{x, xt} Con{y, yt}:
33      Con{U32.xor(x, y), cr.pbkdf2.xor(xt, yt)}
34    case _ _:
35      Nil{}
36
37# acc xor U_(j+1) xor ... for c more iterations, u = U_j
38def cr.pbkdf2.chain(~K: Data, ~compute: K -> B.Octets -> B.Octets, c: Nat, +k: K, u: B.Octets, acc: List<&2, U32>) -> List<&2, U32>:
39  match c:
40    case 0n:
41      acc
42    case 1n+p:
43      +u2 = compute(k, u)
44      cr.pbkdf2.chain(~K, ~compute, p, k, u2, cr.pbkdf2.xor(acc, B.Octets.to_list(u2)))
45
46# T_i, with c the iteration count less one
47def cr.pbkdf2.block(~K: Data, ~compute: K -> B.Octets -> B.Octets, +k: K, salt: B.Octets, c: Nat, i: U32) -> List<&2, U32>:
48  +u1 = compute(k, B.Octets.append(salt, B.Octets.be32(i)))
49  cr.pbkdf2.chain(~K, ~compute, c, k, u1, B.Octets.to_list(u1))
50
51def cr.pbkdf2.head(xs: List<&2, U32>) -> U32:
52  match xs:
53    case Con{h, t}:
54      h
55    case Nil{}:
56      0
57
58def cr.pbkdf2.tail(xs: List<&2, U32>) -> List<&2, U32>:
59  match xs:
60    case Con{h, t}:
61      t
62    case Nil{}:
63      Nil{}
64
65# n more bytes: the rest of the current block cur, then T_(i+1), T_(i+2), ...
66# (a MAC whose tags are empty gives zeros)
67def cr.pbkdf2.out(~K: Data, ~compute: K -> B.Octets -> B.Octets, n: Nat, cur: List<&2, U32>, +k: K, +salt: B.Octets, +c: Nat, +i: U32) -> List<&2, U32>:
68  match n:
69    case 0n:
70      Nil{}
71    case 1n+p:
72      match cur:
73        case Con{h, t}:
74          Con{h, cr.pbkdf2.out(~K, ~compute, p, t, k, salt, c, i)}
75        case Nil{}:
76          +blk = cr.pbkdf2.block(~K, ~compute, k, salt, c, U32.add(i, 1))
77          Con{cr.pbkdf2.head(blk), cr.pbkdf2.out(~K, ~compute, p, cr.pbkdf2.tail(blk), k, salt, c, U32.add(i, 1))}
78
79# The first n bytes of the derived key, under a prepared key k (the MAC's,
80# from the password) and an iteration count c of at least 1, without the
81# checks: T_1 || T_2 || ... cut to n bytes
82def CrPbkdf2.stream(~K: Data, ~compute: K -> B.Octets -> B.Octets, k: K, salt: B.Octets, c: U32, n: Nat) -> B.Octets:
83  B.Octets.of_list(cr.pbkdf2.out(~K, ~compute, n, Nil{}, k, salt, Nat.sub(U32.to_nat(c), 1n), 0))
84
85def cr.pbkdf2.key(~K: Data, ~compute: K -> B.Octets -> B.Octets, kr: Result<&2, &2, Cr.CrError, K>, salt: B.Octets, c: U32, n: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
86  match kr:
87    case Fail{e}:
88      Fail{e}
89    case Done{k}:
90      Done{CrPbkdf2.stream(~K, ~compute, k, salt, c, n)}
91
92def cr.pbkdf2.checked(~K: Data, ~compute: K -> B.Octets -> B.Octets, zero: Bool, fits: Bool, kr: Result<&2, &2, Cr.CrError, K>, salt: B.Octets, c: U32, +n: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
93  match zero:
94    case True{}:
95      Fail{Cr.CrTooShort{0n}}
96    case False{}:
97      match fits:
98        case False{}:
99          Fail{Cr.CrBadOutputLength{n}}
100        case True{}:
101          cr.pbkdf2.key(~K, ~compute, kr, salt, c, n)
102
103def cr.pbkdf2.fits(pos: Bool, +n: Nat, +hlen: Nat) -> Bool:
104  match pos:
105    case True{}:
106      Nat.is_le(Nat.div(Nat.add(n, Nat.sub(hlen, 1n)), hlen), 4294967295n)
107    case False{}:
108      False{}
109
110# DK = PBKDF2(P, S, c, dkLen) over the MAC (~K, ~key, ~compute) with
111# hLen-byte tags (~hlen)
112def CrPbkdf2.pbkdf2(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~compute: K -> B.Octets -> B.Octets, ~hlen: Nat, password: B.Octets, salt: B.Octets, +c: U32, +n: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
113  cr.pbkdf2.checked(~K, ~compute, U32.is_eq(c, 0), cr.pbkdf2.fits(Nat.is_lt(0n, hlen), n, hlen), key(password), salt, c, n)
114
115# The KDF interface's ~derive (secret, salt, info, length) for c iterations;
116# info is unused
117def CrPbkdf2.derive(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~compute: K -> B.Octets -> B.Octets, ~hlen: Nat, ~c: U32, secret: B.Octets, salt: B.Octets, info: B.Octets, n: Nat) -> Result<&2, &2, Cr.CrError, B.Octets>:
118  CrPbkdf2.pbkdf2(~K, ~key, ~compute, ~hlen, secret, salt, c, n)