jwt.bend
bend-kit-jwt@0.4.0.0 · 935 lines · 0 definitions
1# JSON Web Tokens: HS256/384/512, RS256, and ES256 compact JWS sign and verify, claim checks, and JWKS keys over Hairpin. Source: https://github.com/paymog/bend-kit/tree/main/jwt
2import Base
3import bend-kit-crypto@0.2.2.1/crypto.bend as Crypto
4import bend-kit-hairpin@0.4.0.0/hairpin.bend as Hairpin
5import bend-kit-http@0.32.0.0/http.bend as Http
6# By hash, as hairpin imports them: bend-kit-json@0.5.0.1, -bytes@0.3.0.0.
7import bend-kit-json@0.5.0.1/json.bend as Json
8import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
9
10# RFC 7519 JWTs as RFC 7515 compact JWS. A token is ASCII text; header and claims are JSON objects.
11# Times are unix seconds as U32 (to 2106). verify pins one alg: a header alg of "none", or of any other
12# alg, fails. Each key kind serves only its algs, so a PEM public key can never become an HMAC secret.
13
14type Alg is Data:
15 HS256{}
16 HS384{}
17 HS512{}
18 RS256{}
19 ES256{}
20
21# Hmac: the shared secret, at least the digest's size (RFC 7518 §3.2).
22# Pem: a PEM "PUBLIC KEY" to verify, or an unencrypted PEM private key to sign.
23# Rsa, Ec: JWK public key parts as big-endian octets (RFC 7518 §6.3, §6.2 on P-256).
24type Key is Type:
25 Hmac{secret: Bytes.Bytes}
26 Pem{pem: Bytes.Bytes}
27 Rsa{n: Bytes.Bytes, e: Bytes.Bytes}
28 Ec{x: Bytes.Bytes, y: Bytes.Bytes}
29
30type Err is Data:
31 Malformed{}
32 AlgMismatch{}
33 Crit{}
34 KeyType{}
35 WeakKey{}
36 BadSig{}
37 BadClaim{}
38 Expired{}
39 NotYet{}
40 Future{}
41 BadIss{}
42 BadAud{}
43 NoKey{}
44 Crypto{code: U32, why: String}
45 Net{e: Hairpin.Err}
46 Status{code: U32}
47
48# What verify accepts: the one alg, the issuer and audience when Some, and leeway seconds of clock skew.
49type Policy is Data:
50 Policy{alg: Alg, iss: Maybe<&2, String>, aud: Maybe<&2, String>, leeway: U32}
51
52def policy(a: Alg) -> Policy:
53 Policy{a, None{}, None{}, 0}
54
55def iss(p: Policy, s: String) -> Policy:
56 Policy{a, old, u, l} = p
57 Policy{a, Some{s}, u, l}
58
59def aud(p: Policy, s: String) -> Policy:
60 Policy{a, i, old, l} = p
61 Policy{a, i, Some{s}, l}
62
63def leeway(p: Policy, +n: U32) -> Policy:
64 Policy{a, i, u, old} = p
65 Policy{a, i, u, n}
66
67def policy.alg(p: Policy) -> Alg:
68 Policy{a, i, u, l} = p
69 a
70
71def alg.name(a: Alg) -> String:
72 match a:
73 case HS256{}:
74 "HS256"
75 case HS384{}:
76 "HS384"
77 case HS512{}:
78 "HS512"
79 case RS256{}:
80 "RS256"
81 case ES256{}:
82 "ES256"
83
84# ---- base64url (RFC 4648 §5), unpadded, as RFC 7515 §2 requires
85
86def b64u.push(+c: U32, acc: String) -> String:
87 match c:
88 case 61:
89 acc
90 case 43:
91 SCon{'-', acc}
92 case 47:
93 SCon{'_', acc}
94 case _:
95 SCon{Chr{c}, acc}
96
97def b64u.go(s: String, acc: String) -> String:
98 match s:
99 case SNil{}:
100 String.reverse(acc)
101 case SCon{Chr{+c}, t}:
102 b64u.go(t, b64u.push(c, acc))
103
104def b64u(b: Bytes.Bytes) -> String:
105 b64u.go(Bytes.to_base64(b), SNil{})
106
107# The standard alphabet's char for c. '+', '/', '=' and NUL become NUL, which no decoder accepts.
108def unb64u.c(+c: U32) -> U32:
109 match c:
110 case 45:
111 43
112 case 95:
113 47
114 case 43:
115 0
116 case 47:
117 0
118 case 61:
119 0
120 case _:
121 c
122
123# Padding for n mod 4 chars; 1 is never a whole group, so it gets a NUL.
124def unb64u.pad(+r: U32, acc: String) -> String:
125 match r:
126 case 2:
127 SCon{'=', SCon{'=', acc}}
128 case 3:
129 SCon{'=', acc}
130 case 1:
131 SCon{Chr{0}, acc}
132 case _:
133 acc
134
135def unb64u.go(s: String, acc: String, +n: U32) -> String:
136 match s:
137 case SNil{}:
138 String.reverse(unb64u.pad((n .&. 3 : U32), acc))
139 case SCon{Chr{+c}, t}:
140 unb64u.go(t, SCon{Chr{unb64u.c(c)}, acc}, (n + 1 : U32))
141
142def unb64u.same(+s: String, r: Bytes.Bytes & Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
143 (b, c) = r
144 Bool.pick(Maybe<&1, Bytes.Bytes>, String.eq(b64u(c), s), Some{b}, None{})
145
146def unb64u.canon(+s: String, m: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
147 match m:
148 case None{}:
149 None{}
150 case Some{b}:
151 unb64u.same(s, Bytes.slice(b, 0, 4294967295))
152
153# Strict: only the URL-safe alphabet, no '=', and only the canonical text of its octets, so pad bits are 0.
154def unb64u(+s: String) -> Maybe<&1, Bytes.Bytes>:
155 unb64u.canon(s, Bytes.from_base64(unb64u.go(s, SNil{}, 0)))
156
157# ---- JSON members as copyable facts
158
159# A NumericDate (RFC 7519 §2) rounded up to whole seconds and capped at the U32 top, or None when it is
160# negative or has an exponent. Up is exact against a whole now: now >= t iff now >= ceil(t).
161type Lit is Data:
162 LStr{s: String}
163 LNum{t: Maybe<&2, U32>}
164 LStrs{xs: Maybe<&2, List<&2, String>>}
165 LOther{}
166
167# One member: its name as octets, and what the checks need of its value.
168type Field is Data:
169 Field{name: String, val: Lit}
170
171def secs.digit(+acc: U32, +d: U32) -> U32:
172 Bool.pick(U32, Bool.or(U32.is_lt(429496729, acc), Bool.and(U32.is_eq(acc, 429496729), U32.is_lt(5, d))), 4294967295, (acc * 10 + d : U32))
173
174def secs.up(+acc: U32, frac: Bool) -> U32:
175 Bool.pick(U32, Bool.and(frac, U32.is_lt(acc, 4294967295)), (acc + 1 : U32), acc)
176
177# The JSON parser has checked the grammar, so only digits and one '.' need telling apart.
178def secs.go(s: String, +acc: U32, +frac: Bool, +point: Bool, +ok: Bool) -> Maybe<&2, U32>:
179 match s:
180 case SNil{}:
181 Bool.pick(Maybe<&2, U32>, ok, Some{secs.up(acc, frac)}, None{})
182 case SCon{Chr{+c}, t}:
183 +d = Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
184 +dot = U32.is_eq(c, 46)
185 secs.go(t, Bool.pick(U32, Bool.or(point, Bool.not(d)), acc, secs.digit(acc, (c - 48 : U32))),
186 Bool.or(frac, Bool.and(point, Bool.and(d, U32.is_ne(c, 48)))), Bool.or(point, dot),
187 Bool.and(ok, Bool.or(d, Bool.and(dot, Bool.not(point)))))
188
189def secs(s: String) -> Maybe<&2, U32>:
190 secs.go(s, 0, False{}, False{}, True{})
191
192def str.of(v: Json.Val) -> Maybe<&2, String>:
193 match v:
194 case Json.Str{s}:
195 Some{Bytes.to_string(s)}
196 case _:
197 None{}
198
199def strs.push(s: Maybe<&2, String>, acc: Maybe<&2, List<&2, String>>) -> Maybe<&2, List<&2, String>>:
200 match s acc:
201 case Some{x} Some{l}:
202 Some{Con{x, l}}
203 case _ _:
204 None{}
205
206def strs(xs: List<&1, Json.Val>, acc: Maybe<&2, List<&2, String>>) -> Maybe<&2, List<&2, String>>:
207 match xs:
208 case Nil{}:
209 acc
210 case x <> t:
211 strs(t, strs.push(str.of(x), acc))
212
213def lit(v: Json.Val) -> Lit:
214 match v:
215 case Json.Str{s}:
216 LStr{Bytes.to_string(s)}
217 case Json.Num{s}:
218 LNum{secs(Bytes.to_string(s))}
219 case Json.Arr{xs}:
220 LStrs{strs(xs, Some{Nil{}})}
221 case _:
222 LOther{}
223
224# An object's members, names as octets, last first.
225def fields(kvs: List<&1, Bytes.Bytes & Json.Val>, acc: List<&2, Field>) -> List<&2, Field>:
226 match kvs:
227 case Nil{}:
228 acc
229 case (k, v) <> t:
230 fields(t, Con{Field{Bytes.to_string(k), lit(v)}, acc})
231
232def field(l: List<&2, Field>, +k: String) -> Maybe<&2, Lit>:
233 match l:
234 case Nil{}:
235 None{}
236 case Field{n, x} <> t:
237 Bool.pick(Maybe<&2, Lit>, String.eq(n, k), Some{x}, field(t, k))
238
239def has(l: List<&2, Field>, +k: String) -> Bool:
240 match l:
241 case Nil{}:
242 False{}
243 case Field{n, x} <> t:
244 Bool.or(String.eq(n, k), has(t, k))
245
246# RFC 7515 §5.2 allows rejecting repeated names; a second "alg" is how parsers come to disagree.
247def dup(l: List<&2, Field>) -> Bool:
248 match l:
249 case Nil{}:
250 False{}
251 case Con{Field{+n, x}, +t}:
252 Bool.or(has(t, n), dup(t))
253
254def str(m: Maybe<&2, Lit>) -> Maybe<&2, String>:
255 match m:
256 case Some{LStr{s}}:
257 Some{s}
258 case _:
259 None{}
260
261# ---- parsing
262
263# A compact JWS: the header and claim members, the claims, the signing input, and the signature.
264type Parts is Type:
265 Parts{head: List<&2, Field>, facts: List<&2, Field>, claims: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes}
266
267def parse.objs(hf: List<&2, Field>, ff: List<&2, Field>, cv: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes) ->
268 Result<&1, &1, Err, Parts>:
269 +h = hf
270 +f = ff
271 Bool.pick(Result<&1, &1, Err, Parts>, Bool.or(dup(h), dup(f)), Fail{Malformed{}}, Done{Parts{h, f, cv, input, sig}})
272
273def parse.json(h: Maybe<&1, Json.Val>, f: Maybe<&1, Json.Val>, c: Maybe<&1, Json.Val>, input: Bytes.Bytes, sig: Bytes.Bytes) ->
274 Result<&1, &1, Err, Parts>:
275 match h f c:
276 case Some{Json.Obj{hk}} Some{Json.Obj{fk}} Some{cv}:
277 parse.objs(fields(hk, Nil{}), fields(fk, Nil{}), cv, input, sig)
278 case _ _ _:
279 Fail{Malformed{}}
280
281def parse.claims(hb: Bytes.Bytes, r: Bytes.Bytes & Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> Result<&1, &1, Err, Parts>:
282 (c1, c2) = r
283 parse.json(Json.parse.bytes(hb), Json.parse.bytes(c1), Json.parse.bytes(c2), input, sig)
284
285def parse.segs(h: Maybe<&1, Bytes.Bytes>, c: Maybe<&1, Bytes.Bytes>, s: Maybe<&1, Bytes.Bytes>, input: Bytes.Bytes) ->
286 Result<&1, &1, Err, Parts>:
287 match h c s:
288 case Some{hb} Some{cb} Some{sb}:
289 parse.claims(hb, Bytes.slice(cb, 0, 4294967295), input, sb)
290 case _ _ _:
291 Fail{Malformed{}}
292
293def parse.split(xs: List<&2, String>) -> Result<&1, &1, Err, Parts>:
294 match xs:
295 case Con{+h, Con{+c, Con{+s, Nil{}}}}:
296 parse.segs(unb64u(h), unb64u(c), unb64u(s), Bytes.from_string(h ++ "." ++ c))
297 case _:
298 Fail{Malformed{}}
299
300# Three strict base64url segments, the first two JSON objects with no repeated names.
301def parse(token: String) -> Result<&1, &1, Err, Parts>:
302 parse.split(String.split(token, '.'))
303
304# ---- checks
305
306def fail.if(bad: Bool, +e: Err) -> Result<&1, &1, Err, Unit>:
307 match bad:
308 case True{}:
309 Fail{e}
310 case False{}:
311 Done{Unit{}}
312
313def head.alg(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, String>:
314 match m:
315 case Some{LStr{s}}:
316 Done{s}
317 case _:
318 Fail{Malformed{}}
319
320# The header's alg is exactly the pinned one, and it asks for no extension: crit (RFC 7515 §4.1.11) and
321# b64 (RFC 7797) change how the token must be read, and neither is implemented.
322def head.check(+a: Alg, +h: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
323 do Result<&1, &1, Err, Unit>:
324 got : String <- head.alg(field(h, "alg"))
325 u : Unit <- fail.if(Bool.not(String.eq(got, alg.name(a))), AlgMismatch{})
326 fail.if(Bool.or(has(h, "crit"), has(h, "b64")), Crit{})
327
328def when(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, U32>>:
329 match m:
330 case None{}:
331 Done{None{}}
332 case Some{LNum{Some{t}}}:
333 Done{Some{t}}
334 case Some{_}:
335 Fail{BadClaim{}}
336
337def text(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, String>>:
338 match m:
339 case None{}:
340 Done{None{}}
341 case Some{LStr{s}}:
342 Done{Some{s}}
343 case Some{_}:
344 Fail{BadClaim{}}
345
346# RFC 7519 §4.1.3: aud is one string or an array of them.
347def auds(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, List<&2, String>>>:
348 match m:
349 case None{}:
350 Done{None{}}
351 case Some{LStr{s}}:
352 Done{Some{[s]}}
353 case Some{LStrs{Some{xs}}}:
354 Done{Some{xs}}
355 case Some{_}:
356 Fail{BadClaim{}}
357
358# exp (RFC 7519 §4.1.4): now must be before it; late by at least leeway fails.
359def late(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
360 match m:
361 case None{}:
362 False{}
363 case Some{+t}:
364 Bool.and(U32.is_le(t, now), U32.is_le(lw, (now - t : U32)))
365
366# nbf and iat: at most leeway seconds in the future.
367def early(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
368 match m:
369 case None{}:
370 False{}
371 case Some{+t}:
372 Bool.and(U32.is_lt(now, t), U32.is_lt(lw, (t - now : U32)))
373
374def octets(s: String) -> String:
375 Bytes.to_string(Json.utf8(s))
376
377def iss.bad(want: Maybe<&2, String>, got: Maybe<&2, String>) -> Bool:
378 match want got:
379 case None{} _:
380 False{}
381 case Some{w} Some{g}:
382 Bool.not(String.eq(octets(w), g))
383 case Some{w} None{}:
384 True{}
385
386def aud.has(l: List<&2, String>, +a: String) -> Bool:
387 match l:
388 case Nil{}:
389 False{}
390 case x <> t:
391 Bool.or(String.eq(x, a), aud.has(t, a))
392
393# RFC 7519 §4.1.3: a token with an aud that does not name us fails, as does one without aud when we want one.
394def aud.bad(want: Maybe<&2, String>, got: Maybe<&2, List<&2, String>>) -> Bool:
395 match want got:
396 case None{} None{}:
397 False{}
398 case None{} Some{l}:
399 True{}
400 case Some{w} None{}:
401 True{}
402 case Some{w} Some{l}:
403 Bool.not(aud.has(l, octets(w)))
404
405# The registered claims of c at unix time now.
406def claims.check(p: Policy, +now: U32, +c: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
407 Policy{a, +wi, +wa, +lw} = p
408 do Result<&1, &1, Err, Unit>:
409 exp : Maybe<&2, U32> <- when(field(c, "exp"))
410 nbf : Maybe<&2, U32> <- when(field(c, "nbf"))
411 iat : Maybe<&2, U32> <- when(field(c, "iat"))
412 gi : Maybe<&2, String> <- text(field(c, "iss"))
413 ga : Maybe<&2, List<&2, String>> <- auds(field(c, "aud"))
414 u1 : Unit <- fail.if(late(now, lw, exp), Expired{})
415 u2 : Unit <- fail.if(early(now, lw, nbf), NotYet{})
416 u3 : Unit <- fail.if(early(now, lw, iat), Future{})
417 u4 : Unit <- fail.if(iss.bad(wi, gi), BadIss{})
418 fail.if(aud.bad(wa, ga), BadAud{})
419
420def inspect.parts(+p: Policy, +now: U32, r: Result<&1, &1, Err, Parts>) -> Result<&1, &1, Err, Unit>:
421 match r:
422 case Fail{e}:
423 Fail{e}
424 case Done{Parts{+h, +f, v, input, sig}}:
425 do Result<&1, &1, Err, Unit>:
426 u : Unit <- head.check(policy.alg(p), h)
427 claims.check(p, now, f)
428
429# The header and claims of token, without its signature: the pure half of verify.
430def inspect(p: Policy, token: String, +now: U32) -> Result<&1, &1, Err, Unit>:
431 inspect.parts(p, now, parse(token))
432
433# ---- signatures
434
435def crypto.bytes(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, Err, Bytes.Bytes>:
436 match r:
437 case Fail{(c, w)}:
438 Fail{Crypto{c, w}}
439 case Done{(n, b)}:
440 Done{Bytes.Bytes{n, b}}
441
442def crypto.ok(r: Result<&1, &1, U32 & String, Bool>) -> Result<&1, &1, Err, Bool>:
443 match r:
444 case Fail{(c, w)}:
445 Fail{Crypto{c, w}}
446 case Done{b}:
447 Done{b}
448
449def mac.if(weak: Bool, +alg: String, +kn: U32, kb: Array<U32>, +dn: U32, db: Array<U32>) ->
450 IO(Result<&1, &1, Err, Bytes.Bytes>):
451 match weak:
452 case True{}:
453 IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{WeakKey{}})
454 case False{}:
455 do IO<Result<&1, &1, Err, Bytes.Bytes>>:
456 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.hmac.words(alg, kn, kb, dn, db)
457 return crypto.bytes(r)
458
459def mac(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
460 Bytes.Bytes{+kn, kb} = k
461 Bytes.Bytes{+dn, db} = input
462 mac.if(U32.is_lt(kn, min), alg, kn, kb, dn, db)
463
464def mac.cmp(m: Result<&1, &1, Err, Bytes.Bytes>, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
465 match m:
466 case Fail{e}:
467 IO.pure(Result<&1, &1, Err, Bool>, Fail{e})
468 case Done{Bytes.Bytes{+mn, mb}}:
469 Bytes.Bytes{+sn, sb} = sig
470 do IO<Result<&1, &1, Err, Bool>>:
471 ok : Bool <- Crypto.eq.ct.words(mn, mb, sn, sb)
472 return Done{ok}
473
474# The MAC compares in constant time.
475def mac.check(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
476 do IO<Result<&1, &1, Err, Bool>>:
477 m : Result<&1, &1, Err, Bytes.Bytes> <- mac(alg, min, k, input)
478 mac.cmp(m, sig)
479
480def rsa.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
481 Bytes.Bytes{+pn, pb} = p
482 Bytes.Bytes{+dn, db} = input
483 Bytes.Bytes{+sn, sb} = sig
484 do IO<Result<&1, &1, Err, Bool>>:
485 r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
486 return crypto.ok(r)
487
488def rsa.jwk(n: Bytes.Bytes, e: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
489 Bytes.Bytes{+nn, nb} = n
490 Bytes.Bytes{+en, eb} = e
491 Bytes.Bytes{+dn, db} = input
492 Bytes.Bytes{+sn, sb} = sig
493 do IO<Result<&1, &1, Err, Bool>>:
494 r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.jwk.words("SHA256", nn, nb, en, eb, dn, db, sn, sb)
495 return crypto.ok(r)
496
497def ec.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
498 Bytes.Bytes{+pn, pb} = p
499 Bytes.Bytes{+dn, db} = input
500 Bytes.Bytes{+sn, sb} = sig
501 do IO<Result<&1, &1, Err, Bool>>:
502 r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
503 return crypto.ok(r)
504
505def ec.jwk(x: Bytes.Bytes, y: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
506 Bytes.Bytes{+xn, xb} = x
507 Bytes.Bytes{+yn, yb} = y
508 Bytes.Bytes{+dn, db} = input
509 Bytes.Bytes{+sn, sb} = sig
510 do IO<Result<&1, &1, Err, Bool>>:
511 r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.jwk.words("SHA256", xn, xb, yn, yb, dn, db, sn, sb)
512 return crypto.ok(r)
513
514# Does sig sign input under key for alg? A key of the wrong kind fails with KeyType before any crypto.
515def sig.check(a: Alg, key: Key, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
516 match a key:
517 case HS256{} Hmac{k}:
518 mac.check("SHA256", 32, k, input, sig)
519 case HS384{} Hmac{k}:
520 mac.check("SHA384", 48, k, input, sig)
521 case HS512{} Hmac{k}:
522 mac.check("SHA512", 64, k, input, sig)
523 case RS256{} Pem{p}:
524 rsa.pem(p, input, sig)
525 case RS256{} Rsa{n, e}:
526 rsa.jwk(n, e, input, sig)
527 case ES256{} Pem{p}:
528 ec.pem(p, input, sig)
529 case ES256{} Ec{x, y}:
530 ec.jwk(x, y, input, sig)
531 case _ _:
532 IO.pure(Result<&1, &1, Err, Bool>, Fail{KeyType{}})
533
534def rsa.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
535 Bytes.Bytes{+pn, pb} = p
536 Bytes.Bytes{+dn, db} = input
537 do IO<Result<&1, &1, Err, Bytes.Bytes>>:
538 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.rsa.sign.words("SHA256", pn, pb, dn, db)
539 return crypto.bytes(r)
540
541def ec.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
542 Bytes.Bytes{+pn, pb} = p
543 Bytes.Bytes{+dn, db} = input
544 do IO<Result<&1, &1, Err, Bytes.Bytes>>:
545 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.ecdsa.sign.words("SHA256", pn, pb, dn, db)
546 return crypto.bytes(r)
547
548# The signature of input under key for alg. RS256 and ES256 sign with a PEM private key.
549def sig.make(a: Alg, key: Key, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
550 match a key:
551 case HS256{} Hmac{k}:
552 mac("SHA256", 32, k, input)
553 case HS384{} Hmac{k}:
554 mac("SHA384", 48, k, input)
555 case HS512{} Hmac{k}:
556 mac("SHA512", 64, k, input)
557 case RS256{} Pem{p}:
558 rsa.sign(p, input)
559 case ES256{} Pem{p}:
560 ec.sign(p, input)
561 case _ _:
562 IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{KeyType{}})
563
564# ---- sign and verify
565
566def header.kid(m: Maybe<&2, String>) -> List<&1, Bytes.Bytes & Json.Val>:
567 match m:
568 case None{}:
569 Nil{}
570 case Some{k}:
571 [(Json.utf8("kid"), Json.Str{Json.utf8(k)})]
572
573# {"alg":..,"typ":"JWT"}, then "kid" when given.
574def header(a: Alg, kid: Maybe<&2, String>) -> Json.Val:
575 Json.Obj{Con{(Json.utf8("alg"), Json.Str{Json.utf8(alg.name(a))}), Con{(Json.utf8("typ"), Json.Str{Json.utf8("JWT")}), header.kid(kid)}}}
576
577# header.body in base64url, body being the compact JSON claims: the text the signature covers.
578def signing.input(a: Alg, kid: Maybe<&2, String>, body: Bytes.Bytes) -> String:
579 b64u(Json.encode.bytes(header(a, kid))) ++ "." ++ b64u(body)
580
581def sign.done(+input: String, s: Result<&1, &1, Err, Bytes.Bytes>) -> Result<&1, &1, Err, String>:
582 match s:
583 case Fail{e}:
584 Fail{e}
585 case Done{b}:
586 Done{input ++ "." ++ b64u(b)}
587
588# verify accepts only an object with no repeated names, so sign makes no other kind.
589def sign.obj(m: Maybe<&1, Json.Val>) -> Bool:
590 match m:
591 case Some{Json.Obj{kvs}}:
592 Bool.not(dup(fields(kvs, Nil{})))
593 case _:
594 False{}
595
596def sign.if(ok: Bool, +a: Alg, key: Key, kid: Maybe<&2, String>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
597 match ok:
598 case False{}:
599 IO.pure(Result<&1, &1, Err, String>, Fail{BadClaim{}})
600 case True{}:
601 +input = signing.input(a, kid, body)
602 do IO<Result<&1, &1, Err, String>>:
603 s : Result<&1, &1, Err, Bytes.Bytes> <- sig.make(a, key, Bytes.from_string(input))
604 return sign.done(input, s)
605
606def sign.body(+a: Alg, key: Key, kid: Maybe<&2, String>, r: Bytes.Bytes & Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
607 (body, copy) = r
608 sign.if(sign.obj(Json.parse.bytes(copy)), a, key, kid, body)
609
610# A compact token of claims signed with key for a; kid names the key in the header. Claims that are not
611# an object, or repeat a name, fail with BadClaim.
612def sign(+a: Alg, key: Key, kid: Maybe<&2, String>, claims: Json.Val) -> IO(Result<&1, &1, Err, String>):
613 sign.body(a, key, kid, Bytes.slice(Json.encode.bytes(claims), 0, 4294967295))
614
615def claims.done(r: Result<&1, &1, Err, Unit>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
616 match r:
617 case Fail{e}:
618 Fail{e}
619 case Done{u}:
620 Done{v}
621
622def check.sig(ok: Bool, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
623 match ok:
624 case False{}:
625 Fail{BadSig{}}
626 case True{}:
627 claims.done(claims.check(p, now, f), v)
628
629def check.done(s: Result<&1, &1, Err, Bool>, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) ->
630 Result<&1, &1, Err, Json.Val>:
631 match s:
632 case Fail{e}:
633 Fail{e}
634 case Done{ok}:
635 check.sig(ok, p, now, f, v)
636
637def check.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, key: Key, +now: U32, +f: List<&2, Field>, v: Json.Val,
638 input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Json.Val>):
639 match ok:
640 case Fail{e}:
641 IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
642 case Done{u}:
643 do IO<Result<&1, &1, Err, Json.Val>>:
644 s : Result<&1, &1, Err, Bool> <- sig.check(policy.alg(p), key, input, sig)
645 return check.done(s, p, now, f, v)
646
647# The pinned alg, then the signature, then the claims.
648def check(+p: Policy, key: Key, +now: U32, parts: Parts) -> IO(Result<&1, &1, Err, Json.Val>):
649 Parts{+h, +f, v, input, sig} = parts
650 check.pinned(head.check(policy.alg(p), h), p, key, now, f, v, input, sig)
651
652def verify.parsed(+p: Policy, key: Key, +now: U32, r: Result<&1, &1, Err, Parts>) -> IO(Result<&1, &1, Err, Json.Val>):
653 match r:
654 case Fail{e}:
655 IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
656 case Done{parts}:
657 check(p, key, now, parts)
658
659# The claims of token when it is signed by key under p's alg and its claims hold at unix time now.
660def verify(+p: Policy, key: Key, token: String, +now: U32) -> IO(Result<&1, &1, Err, Json.Val>):
661 verify.parsed(p, key, now, parse(token))
662
663# ---- JWKS (RFC 7517)
664
665# A usable public key from a set: its kid, RSA or EC P-256, its alg ("" when the set gives none), and its
666# two base64url parts (n and e, or x and y).
667type Jwk is Data:
668 Jwk{kid: String, rsa: Bool, alg: String, a: String, b: String}
669
670def jwk.two(+rsa: Bool, +kid: String, +alg: String, a: Maybe<&2, String>, b: Maybe<&2, String>) -> Maybe<&2, Jwk>:
671 match a b:
672 case Some{x} Some{y}:
673 Some{Jwk{kid, rsa, alg, x, y}}
674 case _ _:
675 None{}
676
677# An alg member that is not a string can match no pinned alg.
678def jwk.alg(m: Maybe<&2, Lit>) -> String:
679 match m:
680 case None{}:
681 ""
682 case Some{LStr{s}}:
683 s
684 case Some{_}:
685 "?"
686
687def jwk.use(m: Maybe<&2, Lit>) -> Maybe<&2, Unit>:
688 match m:
689 case None{}:
690 Some{Unit{}}
691 case Some{LStr{s}}:
692 Bool.pick(Maybe<&2, Unit>, String.eq(s, "sig"), Some{Unit{}}, None{})
693 case Some{_}:
694 None{}
695
696def jwk.kty(+kty: String, +kid: String, +f: List<&2, Field>) -> Maybe<&2, Jwk>:
697 +alg = jwk.alg(field(f, "alg"))
698 +ec = Bool.and(String.eq(kty, "EC"), String.eq(Maybe.default(&2, String, str(field(f, "crv")), ""), "P-256"))
699 Bool.pick(Maybe<&2, Jwk>, String.eq(kty, "RSA"), jwk.two(True{}, kid, alg, str(field(f, "n")), str(field(f, "e"))),
700 Bool.pick(Maybe<&2, Jwk>, ec, jwk.two(False{}, kid, alg, str(field(f, "x")), str(field(f, "y"))), None{}))
701
702def jwk.fields(+f: List<&2, Field>) -> Maybe<&2, Jwk>:
703 do Maybe<&2, Jwk>:
704 u : Unit <- Bool.pick(Maybe<&2, Unit>, dup(f), None{}, Some{Unit{}})
705 kty : String <- str(field(f, "kty"))
706 kid : String <- str(field(f, "kid"))
707 s : Unit <- jwk.use(field(f, "use"))
708 jwk.kty(kty, kid, f)
709
710def jwk.of(v: Json.Val) -> Maybe<&2, Jwk>:
711 match v:
712 case Json.Obj{kvs}:
713 jwk.fields(fields(kvs, Nil{}))
714 case _:
715 None{}
716
717def jwk.push(m: Maybe<&2, Jwk>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
718 match m:
719 case None{}:
720 acc
721 case Some{k}:
722 Con{k, acc}
723
724def jwks.go(xs: List<&1, Json.Val>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
725 match xs:
726 case Nil{}:
727 List.reverse(&2, Jwk, acc)
728 case x <> t:
729 jwks.go(t, jwk.push(jwk.of(x), acc))
730
731def jwks.arr(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
732 match m:
733 case Some{Json.Arr{xs}}:
734 Some{jwks.go(xs, Nil{})}
735 case _:
736 None{}
737
738def jwks.doc(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
739 match m:
740 case Some{v}:
741 jwks.arr(Json.get(v, "keys"))
742 case None{}:
743 None{}
744
745# The signing keys of a JWK Set document; members it cannot use (enc keys, other curves, oct) are skipped.
746# None when the document is not {"keys": [...]}.
747def jwks.parse(b: Bytes.Bytes) -> Maybe<&2, List<&2, Jwk>>:
748 jwks.doc(Json.parse.bytes(b))
749
750def fam(a: Alg) -> U32:
751 match a:
752 case RS256{}:
753 1
754 case ES256{}:
755 2
756 case _:
757 0
758
759def jwk.fits(k: Jwk, +kid: String, +a: Alg) -> Bool:
760 Jwk{k2, +rsa, +ka, x, y} = k
761 Bool.and(Bool.and(String.eq(k2, kid), U32.is_eq(fam(a), Bool.pick(U32, rsa, 1, 2))),
762 Bool.or(String.eq(ka, ""), String.eq(ka, alg.name(a))))
763
764# The first key named kid that can check alg a. RFC 7515 §4.1.4 leaves kid matching to exact comparison.
765def jwk.pick(ks: List<&2, Jwk>, +kid: String, +a: Alg) -> Maybe<&2, Jwk>:
766 match ks:
767 case Nil{}:
768 None{}
769 case Con{+k, t}:
770 Bool.pick(Maybe<&2, Jwk>, jwk.fits(k, kid, a), Some{k}, jwk.pick(t, kid, a))
771
772def jwk.key.of(rsa: Bool, a: Maybe<&1, Bytes.Bytes>, b: Maybe<&1, Bytes.Bytes>) -> Result<&1, &1, Err, Key>:
773 match rsa a b:
774 case True{} Some{n} Some{e}:
775 Done{Rsa{n, e}}
776 case False{} Some{x} Some{y}:
777 Done{Ec{x, y}}
778 case _ _ _:
779 Fail{Malformed{}}
780
781# A set member as a verify key.
782def jwk.key(k: Jwk) -> Result<&1, &1, Err, Key>:
783 Jwk{kid, +rsa, alg, +a, +b} = k
784 jwk.key.of(rsa, unb64u(a), unb64u(b))
785
786def jwk.found(m: Maybe<&2, Jwk>) -> Result<&1, &1, Err, Key>:
787 match m:
788 case None{}:
789 Fail{NoKey{}}
790 case Some{k}:
791 jwk.key(k)
792
793# A cached key set from the caller's own trusted url; a token never picks the url (jku and x5u are ignored).
794# live: fetched once; at: the unix time of the last good fetch; ttl: seconds it stays fresh;
795# tried: the unix time of the last fetch, good or not.
796type Jwks is Data:
797 Jwks{url: String, ttl: U32, live: Bool, at: U32, tried: Maybe<&2, U32>, keys: List<&2, Jwk>}
798
799def jwks(url: String, +ttl: U32) -> Jwks:
800 Jwks{url, ttl, False{}, 0, None{}, Nil{}}
801
802def jwks.keys(s: Jwks) -> List<&2, Jwk>:
803 Jwks{u, t, l, a, tr, ks} = s
804 ks
805
806def fetch.keys(m: Maybe<&2, List<&2, Jwk>>, c: Hairpin.Client, s: Jwks, +now: U32) -> Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
807 match m:
808 case None{}:
809 (c, s, Fail{Malformed{}})
810 case Some{ks}:
811 Jwks{url, ttl, live, at, tried, old} = s
812 (c, Jwks{url, ttl, True{}, now, tried, ks}, Done{Unit{}})
813
814def fetch.body(ok: Bool, +status: U32, c: Hairpin.Client, s: Jwks, +now: U32, b: Bytes.Bytes) ->
815 Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
816 match ok:
817 case False{}:
818 (c, s, Fail{Status{status}})
819 case True{}:
820 fetch.keys(jwks.parse(b), c, s, now)
821
822def fetch.res(c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Hairpin.Err, Http.Res>) ->
823 Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
824 match r:
825 case Fail{e}:
826 (c, s, Fail{Net{e}})
827 case Done{Http.Res{+status, h, b}}:
828 fetch.body(U32.is_eq(status, 200), status, c, s, now, b)
829
830def fetch.done(s: Jwks, +now: U32, x: Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res>) ->
831 Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
832 (c, r) = x
833 fetch.res(c, s, now, r)
834
835# GET the set now. On any failure the client and the old keys come back, with only tried moved to now.
836def fetch(c: Hairpin.Client, s: Jwks, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>):
837 Jwks{+url, ttl, live, at, old, ks} = s
838 do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>>:
839 x : Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res> <- Hairpin.get(c, url)
840 return fetch.done(Jwks{url, ttl, live, at, Some{now}, ks}, now, x)
841
842def key.after.r(r: Result<&1, &1, Err, Unit>, c: Hairpin.Client, +s: Jwks, +kid: String, +a: Alg) ->
843 Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
844 match r:
845 case Fail{e}:
846 (c, s, Fail{e})
847 case Done{u}:
848 (c, s, jwk.found(jwk.pick(jwks.keys(s), kid, a)))
849
850def key.after(+kid: String, +a: Alg, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>) ->
851 Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
852 (c, s, r) = x
853 key.after.r(r, c, s, kid, a)
854
855def key.refetch(go: Bool, c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) ->
856 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
857 match go:
858 case False{}:
859 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, Fail{NoKey{}}))
860 case True{}:
861 do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Key>>:
862 x : Hairpin.Client & Jwks & Result<&1, &1, Err, Unit> <- fetch(c, s, now)
863 return key.after(kid, a, x)
864
865def key.go(cached: Bool, +go: Bool, c: Hairpin.Client, s: Jwks, found: Maybe<&2, Jwk>, +kid: String, +a: Alg, +now: U32) ->
866 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
867 match cached:
868 case True{}:
869 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, jwk.found(found)))
870 case False{}:
871 key.refetch(go, c, s, kid, a, now)
872
873def since(+now: U32, m: Maybe<&2, U32>) -> U32:
874 match m:
875 case None{}:
876 4294967295
877 case Some{+t}:
878 Bool.pick(U32, U32.is_le(t, now), (now - t : U32), 0)
879
880# The verify key named kid for alg a. A known key stays usable through the 60 s fetch cooldown even
881# when ttl is shorter. After that, refresh a stale set or an unknown kid at most once a minute.
882# ponytail: fixed 60 s cooldown; make it a Jwks field if an issuer rotates faster.
883def key(c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
884 Jwks{+url, +ttl, +live, +at, +tried, +ks} = s
885 +found = jwk.pick(ks, kid, a)
886 +fresh = Bool.and(live, Bool.and(U32.is_le(at, now), U32.is_lt((now - at : U32), Bool.pick(U32, U32.is_lt(ttl, 60), 60, ttl))))
887 +cached = Bool.and(fresh, Maybe.is_some(&2, Jwk, found))
888 key.go(cached, U32.is_le(60, since(now, tried)), c, Jwks{url, ttl, live, at, tried, ks}, found, kid, a, now)
889
890def jwks.run(r: Result<&1, &1, Err, Key>, c: Hairpin.Client, s: Jwks, +p: Policy, +now: U32, parts: Parts) ->
891 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
892 match r:
893 case Fail{e}:
894 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
895 case Done{k}:
896 do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
897 v : Result<&1, &1, Err, Json.Val> <- check(p, k, now, parts)
898 return (c, s, v)
899
900def jwks.keyed(+p: Policy, +now: U32, parts: Parts, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Key>) ->
901 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
902 (c, s, r) = x
903 jwks.run(r, c, s, p, now, parts)
904
905def jwks.kid(k: Maybe<&2, String>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, parts: Parts) ->
906 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
907 match k:
908 case None{}:
909 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{NoKey{}}))
910 case Some{+kid}:
911 do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
912 x : Hairpin.Client & Jwks & Result<&1, &1, Err, Key> <- key(c, s, kid, policy.alg(p), now)
913 jwks.keyed(p, now, parts, x)
914
915def jwks.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, +h: List<&2, Field>,
916 parts: Parts) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
917 match ok:
918 case Fail{e}:
919 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
920 case Done{u}:
921 jwks.kid(str(field(h, "kid")), p, c, s, now, parts)
922
923def jwks.parsed(+p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Err, Parts>) ->
924 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
925 match r:
926 case Fail{e}:
927 IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
928 case Done{Parts{+h, f, v, input, sig}}:
929 jwks.pinned(head.check(policy.alg(p), h), p, c, s, now, h, Parts{h, f, v, input, sig})
930
931# verify with the key the token's kid names in the set. The alg is pinned before any fetch.
932# The client and the set (refreshed or not) always come back.
933def verify.jwks(+p: Policy, c: Hairpin.Client, s: Jwks, token: String, +now: U32) ->
934 IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
935 jwks.parsed(p, c, s, now, parse(token))