src/crypto/argon2/phc.bend

bend-collections-laws-crypto@1.0.0.0 · 387 lines · 61 definitions

1import Base
2
3# The PHC string format of an Argon2id hash:
4#
5#   $argon2id$v=19$m=<m>,t=<t>,p=<p>$<salt>$<hash>
6#
7# with m, t, p in decimal and the salt and hash in standard base64 (RFC 4648
8# section 4 alphabet) without padding, as the reference implementation and
9# argon2-cffi write it. parse accepts exactly the strings format writes, up to
10# leading zeros in the numbers; base64 must be canonical (unused low bits zero).
11#
12# Bytes are U32 values below 256. Base64 is computed through 2-bit crumbs: a
13# byte is four crumbs (high first), a base64 digit three, so encoding and
14# decoding only regroup crumbs.
15
16type Phc is Data:
17  Phc{m: Nat, t: Nat, p: Nat, salt: List<&2, U32>, hash: List<&2, U32>}
18
19# A number read and the rest of the string.
20type Got is Data:
21  Got{value: Nat, rest: String}
22
23# A string cut at a '$': before and after it.
24type Cut is Data:
25  Cut{before: String, after: String}
26
27# ---------------------------------------------------------------- crumbs
28
29# The crumbs of a byte n, high first: n = ((c3 * 4 + c2) * 4 + c1) * 4 + c0.
30def c0(+b: U32) -> U32:
31  U32.from_nat(Nat.mod(U32.to_nat(b), 4n))
32
33def c1(+b: U32) -> U32:
34  U32.from_nat(Nat.mod(Nat.div(U32.to_nat(b), 4n), 4n))
35
36def c2(+b: U32) -> U32:
37  U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(b), 4n), 4n), 4n))
38
39def c3(+b: U32) -> U32:
40  U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(b), 4n), 4n), 4n))
41
42# The byte of four crumbs, high first.
43def byte_of(+w: U32, +x: U32, +y: U32, +z: U32) -> U32:
44  U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(U32.to_nat(w), 4n), U32.to_nat(x)), 4n), U32.to_nat(y)), 4n), U32.to_nat(z)))
45
46# The base64 digit value of three crumbs, high first, and back.
47def sext(+x: U32, +y: U32, +z: U32) -> U32:
48  U32.or(U32.shln(x, 4n), U32.or(U32.shln(y, 2n), z))
49
50def su(+s: U32) -> U32:
51  U32.shrn(s, 4n)
52
53def sv(+s: U32) -> U32:
54  U32.and(U32.shrn(s, 2n), 3)
55
56def sw(+s: U32) -> U32:
57  U32.and(s, 3)
58
59def digit_last(+s: U32, is62: Bool) -> U32:
60  match is62:
61    case True{}:
62      43
63    case False{}:
64      47
65
66# ---------------------------------------------------------------- base64 digits
67
68def digit_hi(+s: U32, lt62: Bool) -> U32:
69  match lt62:
70    case True{}:
71      U32.sub(s, 4)
72    case False{}:
73      digit_last(s, U32.is_eq(s, 62))
74
75def digit_mid(+s: U32, lt52: Bool) -> U32:
76  match lt52:
77    case True{}:
78      U32.add(s, 71)
79    case False{}:
80      digit_hi(s, U32.is_lt(s, 62))
81
82def digit_code(+s: U32, lt26: Bool) -> U32:
83  match lt26:
84    case True{}:
85      U32.add(s, 65)
86    case False{}:
87      digit_mid(s, U32.is_lt(s, 52))
88
89# The character of digit value s < 64: A-Z, a-z, 0-9, +, /.
90def digit(+s: U32) -> Char:
91  Chr{digit_code(s, U32.is_lt(s, 26))}
92
93def in_range(+x: U32, +lo: U32, +hi: U32) -> Bool:
94  Bool.and(U32.is_le(lo, x), U32.is_le(x, hi))
95
96def value_slash(slash: Bool) -> Maybe<&2, U32>:
97  match slash:
98    case True{}:
99      Some{63}
100    case False{}:
101      None{}
102
103def value_sym(+x: U32, plus: Bool) -> Maybe<&2, U32>:
104  match plus:
105    case True{}:
106      Some{62}
107    case False{}:
108      value_slash(U32.is_eq(x, 47))
109
110def value_num(+x: U32, num: Bool) -> Maybe<&2, U32>:
111  match num:
112    case True{}:
113      Some{U32.add(x, 4)}
114    case False{}:
115      value_sym(x, U32.is_eq(x, 43))
116
117def value_low(+x: U32, low: Bool) -> Maybe<&2, U32>:
118  match low:
119    case True{}:
120      Some{U32.sub(x, 71)}
121    case False{}:
122      value_num(x, in_range(x, 48, 57))
123
124def value_code(+x: U32, up: Bool) -> Maybe<&2, U32>:
125  match up:
126    case True{}:
127      Some{U32.sub(x, 65)}
128    case False{}:
129      value_low(x, in_range(x, 97, 122))
130
131# The value of a base64 character, or None.
132def value(c: Char) -> Maybe<&2, U32>:
133  match c:
134    case Chr{+x}:
135      value_code(x, in_range(x, 65, 90))
136
137# ---------------------------------------------------------------- base64
138
139def enc1(+a: U32) -> String:
140  SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), 0, 0)), SNil{}}}
141
142def enc2(+a: U32, +b: U32) -> String:
143  SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), c3(b), c2(b))), SCon{digit(sext(c1(b), c0(b), 0)), SNil{}}}}
144
145def enc3(+a: U32, +b: U32, +c: U32, rest: String) -> String:
146  SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), c3(b), c2(b))), SCon{digit(sext(c1(b), c0(b), c3(c))), SCon{digit(sext(c2(c), c1(c), c0(c))), rest}}}}
147
148# Standard base64 without padding.
149def b64(bs: List<&2, U32>) -> String:
150  match bs:
151    case Nil{}:
152      SNil{}
153    case a <> Nil{}:
154      enc1(a)
155    case a <> b <> Nil{}:
156      enc2(a, b)
157    case a <> b <> c <> rest:
158      enc3(a, b, c, b64(rest))
159
160def dec2_fin(+x: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>:
161  match ok:
162    case True{}:
163      Some{[x]}
164    case False{}:
165      None{}
166
167def dec2(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>) -> Maybe<&2, List<&2, U32>>:
168  match ma mb:
169    case Some{+a} Some{+b}:
170      dec2_fin(byte_of(su(a), sv(a), sw(a), su(b)), Bool.and(U32.is_eq(sv(b), 0), U32.is_eq(sw(b), 0)))
171    case _ _:
172      None{}
173
174def dec3_fin(+x: U32, +y: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>:
175  match ok:
176    case True{}:
177      Some{[x, y]}
178    case False{}:
179      None{}
180
181def dec3(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>, mc: Maybe<&2, U32>) -> Maybe<&2, List<&2, U32>>:
182  match ma mb mc:
183    case Some{+a} Some{+b} Some{+c}:
184      dec3_fin(byte_of(su(a), sv(a), sw(a), su(b)), byte_of(sv(b), sw(b), su(c), sv(c)), U32.is_eq(sw(c), 0))
185    case _ _ _:
186      None{}
187
188def dec4(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>, mc: Maybe<&2, U32>, md: Maybe<&2, U32>, mr: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
189  match ma mb mc md mr:
190    case Some{+a} Some{+b} Some{+c} Some{+d} Some{rest}:
191      Some{byte_of(su(a), sv(a), sw(a), su(b)) <> byte_of(sv(b), sw(b), su(c), sv(c)) <> byte_of(sw(c), su(d), sv(d), sw(d)) <> rest}
192    case _ _ _ _ _:
193      None{}
194
195# The bytes of canonical unpadded base64, or None.
196def unb64(s: String) -> Maybe<&2, List<&2, U32>>:
197  match s:
198    case SNil{}:
199      Some{Nil{}}
200    case SCon{a, SNil{}}:
201      None{}
202    case SCon{a, SCon{b, SNil{}}}:
203      dec2(value(a), value(b))
204    case SCon{a, SCon{b, SCon{c, SNil{}}}}:
205      dec3(value(a), value(b), value(c))
206    case SCon{a, SCon{b, SCon{c, SCon{d, rest}}}}:
207      dec4(value(a), value(b), value(c), value(d), unb64(rest))
208
209# ---------------------------------------------------------------- decimal
210
211def dchar(+d: Nat) -> Char:
212  Chr{U32.add(48, U32.from_nat(d))}
213
214# The decimal digits of n before acc; fuel bounds the number of digits and
215# last says n < 10.
216def dec_go(fuel: Nat, +n: Nat, acc: String, last: Bool) -> String:
217  match fuel last:
218    case 0n _:
219      acc
220    case 1n+f True{}:
221      SCon{dchar(n), acc}
222    case 1n+f False{}:
223      +q = Nat.div(n, 10n)
224      dec_go(f, q, SCon{dchar(Nat.mod(n, 10n)), acc}, Nat.is_lt(q, 10n))
225
226# n in decimal, without leading zeros.
227def decimal(+n: Nat) -> String:
228  dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n))
229
230def is_digit(+x: U32) -> Bool:
231  in_range(x, 48, 57)
232
233def starts_digit(s: String) -> Bool:
234  match s:
235    case SNil{}:
236      False{}
237    case SCon{Chr{+x}, rest}:
238      is_digit(x)
239
240# Digits from s on top of v (d says s starts with a digit); the value and the rest.
241def read_go(s: String, +v: Nat, d: Bool) -> Got:
242  match s d:
243    case SNil{} _:
244      Got{v, SNil{}}
245    case SCon{Chr{+x}, +rest} True{}:
246      read_go(rest, Nat.add(Nat.mul(v, 10n), U32.to_nat(U32.sub(x, 48))), starts_digit(rest))
247    case SCon{c, rest} False{}:
248      Got{v, SCon{c, rest}}
249
250def read_check(s: String, first: Bool) -> Maybe<&2, Got>:
251  match first:
252    case True{}:
253      Some{read_go(s, 0n, True{})}
254    case False{}:
255      None{}
256
257# A decimal number (at least one digit) and the rest.
258def read(+s: String) -> Maybe<&2, Got>:
259  read_check(s, starts_digit(s))
260
261# ---------------------------------------------------------------- the string
262
263def same_char(a: Char, b: Char) -> Bool:
264  match a b:
265    case Chr{x} Chr{y}:
266      U32.is_eq(x, y)
267
268def heads(+lit: String, +s: String) -> Bool:
269  match lit s:
270    case SCon{a, lt} SCon{b, st}:
271      same_char(a, b)
272    case _ _:
273      False{}
274
275# s without the prefix lit, or None (same says the first characters agree).
276def strip_go(lit: String, s: String, same: Bool) -> Maybe<&2, String>:
277  match lit s same:
278    case SNil{} _ _:
279      Some{s}
280    case SCon{a, lt} SNil{} _:
281      None{}
282    case SCon{a, +lt} SCon{b, +st} True{}:
283      strip_go(lt, st, heads(lt, st))
284    case SCon{a, lt} SCon{b, st} False{}:
285      None{}
286
287def strip(+lit: String, +s: String) -> Maybe<&2, String>:
288  strip_go(lit, s, heads(lit, s))
289
290def dollar(s: String) -> Bool:
291  match s:
292    case SCon{Chr{+x}, rest}:
293      U32.is_eq(x, 36)
294    case SNil{}:
295      False{}
296
297def field_cons(+x: U32, r: Maybe<&2, Cut>) -> Maybe<&2, Cut>:
298  match r:
299    case None{}:
300      None{}
301    case Some{Cut{a, b}}:
302      Some{Cut{SCon{Chr{x}, a}, b}}
303
304# The characters before the first '$' and what follows it, or None (d says s starts with '$').
305def field_go(s: String, d: Bool) -> Maybe<&2, Cut>:
306  match s d:
307    case SNil{} _:
308      None{}
309    case SCon{c, rest} True{}:
310      Some{Cut{SNil{}, rest}}
311    case SCon{Chr{+x}, +rest} False{}:
312      field_cons(x, field_go(rest, dollar(rest)))
313
314def field(+s: String) -> Maybe<&2, Cut>:
315  field_go(s, dollar(s))
316
317def format(x: Phc) -> String:
318  match x:
319    case Phc{m, t, p, salt, hash}:
320      String.concat(["$argon2id$v=19$m=", decimal(m), ",t=", decimal(t), ",p=", decimal(p), "$", b64(salt), "$", b64(hash)])
321
322def parse_hash(+m: Nat, +t: Nat, +p: Nat, salt: Maybe<&2, List<&2, U32>>, hash: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Phc>:
323  match salt hash:
324    case Some{s} Some{h}:
325      Some{Phc{m, t, p, s, h}}
326    case _ _:
327      None{}
328
329def parse_salt(+m: Nat, +t: Nat, +p: Nat, r: Maybe<&2, Cut>) -> Maybe<&2, Phc>:
330  match r:
331    case None{}:
332      None{}
333    case Some{Cut{s, h}}:
334      parse_hash(m, t, p, unb64(s), unb64(h))
335
336def parse_p2(+m: Nat, +t: Nat, +p: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>:
337  match r:
338    case None{}:
339      None{}
340    case Some{rest}:
341      parse_salt(m, t, p, field(rest))
342
343def parse_p(+m: Nat, +t: Nat, r: Maybe<&2, Got>) -> Maybe<&2, Phc>:
344  match r:
345    case None{}:
346      None{}
347    case Some{Got{+p, rest}}:
348      parse_p2(m, t, p, strip("$", rest))
349
350def parse_t2(+m: Nat, +t: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>:
351  match r:
352    case None{}:
353      None{}
354    case Some{rest}:
355      parse_p(m, t, read(rest))
356
357def parse_t(+m: Nat, r: Maybe<&2, Got>) -> Maybe<&2, Phc>:
358  match r:
359    case None{}:
360      None{}
361    case Some{Got{+t, rest}}:
362      parse_t2(m, t, strip(",p=", rest))
363
364def parse_m2(+m: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>:
365  match r:
366    case None{}:
367      None{}
368    case Some{rest}:
369      parse_t(m, read(rest))
370
371def parse_m(r: Maybe<&2, Got>) -> Maybe<&2, Phc>:
372  match r:
373    case None{}:
374      None{}
375    case Some{Got{+m, rest}}:
376      parse_m2(m, strip(",t=", rest))
377
378def parse_head(r: Maybe<&2, String>) -> Maybe<&2, Phc>:
379  match r:
380    case None{}:
381      None{}
382    case Some{rest}:
383      parse_m(read(rest))
384
385# The fields of an Argon2id version 19 PHC string, or None.
386def parse(s: String) -> Maybe<&2, Phc>:
387  parse_head(strip("$argon2id$v=19$m=", s))