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