jwt.bend

bend-kit-jwt@0.11.0.1 · 925 lines · 122 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.2/crypto.bend as Crypto
4import bend-kit-hairpin@0.13.0.1/hairpin.bend as Hairpin
5import bend-kit-http@0.38.1.1/http.bend as Http
6import bend-kit-json@0.7.0.0/json.bend as Json
7import bend-kit-bytes@0.3.3.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
245def str(m: Maybe<&2, Lit>) -> Maybe<&2, String>:
246  match m:
247    case Some{LStr{s}}:
248      Some{s}
249    case _:
250      None{}
251
252# ---- parsing
253
254# A compact JWS: the header and claim members, the claims, the signing input, and the signature.
255type Parts is Type:
256  Parts{head: List<&2, Field>, facts: List<&2, Field>, claims: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes}
257
258# RFC 7515 §5.2 allows rejecting repeated names; a second "alg" is how parsers come to disagree.
259# parse.claims rejects them at every depth with Json.unique.parsed before members get here.
260def parse.json(h: Maybe<&1, Json.Val>, f: Maybe<&1, Json.Val>, c: Maybe<&1, Json.Val>, input: Bytes.Bytes, sig: Bytes.Bytes) ->
261    Result<&1, &1, Err, Parts>:
262  match h f c:
263    case Some{Json.Obj{hk}} Some{Json.Obj{fk}} Some{cv}:
264      Done{Parts{fields(hk, Nil{}), fields(fk, Nil{}), cv, input, sig}}
265    case _ _ _:
266      Fail{Malformed{}}
267
268def parse.claims(hb: Bytes.Bytes, r: Bytes.Bytes & Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> Result<&1, &1, Err, Parts>:
269  (c1, c2) = r
270  parse.json(Json.unique.parsed(Json.parse.bytes(hb)), Json.unique.parsed(Json.parse.bytes(c1)), Json.parse.bytes(c2), input, sig)
271
272def parse.segs(h: Maybe<&1, Bytes.Bytes>, c: Maybe<&1, Bytes.Bytes>, s: Maybe<&1, Bytes.Bytes>, input: Bytes.Bytes) ->
273    Result<&1, &1, Err, Parts>:
274  match h c s:
275    case Some{hb} Some{cb} Some{sb}:
276      parse.claims(hb, Bytes.slice(cb, 0, 4294967295), input, sb)
277    case _ _ _:
278      Fail{Malformed{}}
279
280def parse.split(xs: List<&2, String>) -> Result<&1, &1, Err, Parts>:
281  match xs:
282    case Con{+h, Con{+c, Con{+s, Nil{}}}}:
283      parse.segs(unb64u(h), unb64u(c), unb64u(s), Bytes.from_string(h ++ "." ++ c))
284    case _:
285      Fail{Malformed{}}
286
287# Three strict base64url segments, the first two JSON objects with no repeated names.
288def parse(token: String) -> Result<&1, &1, Err, Parts>:
289  parse.split(String.split(token, '.'))
290
291# ---- checks
292
293def fail.if(bad: Bool, +e: Err) -> Result<&1, &1, Err, Unit>:
294  match bad:
295    case True{}:
296      Fail{e}
297    case False{}:
298      Done{Unit{}}
299
300def head.alg(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, String>:
301  match m:
302    case Some{LStr{s}}:
303      Done{s}
304    case _:
305      Fail{Malformed{}}
306
307# The header's alg is exactly the pinned one, and it asks for no extension: crit (RFC 7515 §4.1.11) and
308# b64 (RFC 7797) change how the token must be read, and neither is implemented.
309def head.check(+a: Alg, +h: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
310  do Result<&1, &1, Err, Unit>:
311    got : String <- head.alg(field(h, "alg"))
312    u : Unit <- fail.if(Bool.not(String.eq(got, alg.name(a))), AlgMismatch{})
313    fail.if(Bool.or(has(h, "crit"), has(h, "b64")), Crit{})
314
315def when(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, U32>>:
316  match m:
317    case None{}:
318      Done{None{}}
319    case Some{LNum{Some{t}}}:
320      Done{Some{t}}
321    case Some{_}:
322      Fail{BadClaim{}}
323
324def text(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, String>>:
325  match m:
326    case None{}:
327      Done{None{}}
328    case Some{LStr{s}}:
329      Done{Some{s}}
330    case Some{_}:
331      Fail{BadClaim{}}
332
333# RFC 7519 §4.1.3: aud is one string or an array of them.
334def auds(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, List<&2, String>>>:
335  match m:
336    case None{}:
337      Done{None{}}
338    case Some{LStr{s}}:
339      Done{Some{[s]}}
340    case Some{LStrs{Some{xs}}}:
341      Done{Some{xs}}
342    case Some{_}:
343      Fail{BadClaim{}}
344
345# exp (RFC 7519 §4.1.4): now must be before it; late by at least leeway fails.
346def late(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
347  match m:
348    case None{}:
349      False{}
350    case Some{+t}:
351      Bool.and(U32.is_le(t, now), U32.is_le(lw, (now - t : U32)))
352
353# nbf and iat: at most leeway seconds in the future.
354def early(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
355  match m:
356    case None{}:
357      False{}
358    case Some{+t}:
359      Bool.and(U32.is_lt(now, t), U32.is_lt(lw, (t - now : U32)))
360
361def octets(s: String) -> String:
362  Bytes.to_string(Json.utf8(s))
363
364def iss.bad(want: Maybe<&2, String>, got: Maybe<&2, String>) -> Bool:
365  match want got:
366    case None{} _:
367      False{}
368    case Some{w} Some{g}:
369      Bool.not(String.eq(octets(w), g))
370    case Some{w} None{}:
371      True{}
372
373def aud.has(l: List<&2, String>, +a: String) -> Bool:
374  match l:
375    case Nil{}:
376      False{}
377    case x <> t:
378      Bool.or(String.eq(x, a), aud.has(t, a))
379
380# 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.
381def aud.bad(want: Maybe<&2, String>, got: Maybe<&2, List<&2, String>>) -> Bool:
382  match want got:
383    case None{} None{}:
384      False{}
385    case None{} Some{l}:
386      True{}
387    case Some{w} None{}:
388      True{}
389    case Some{w} Some{l}:
390      Bool.not(aud.has(l, octets(w)))
391
392# The registered claims of c at unix time now.
393def claims.check(p: Policy, +now: U32, +c: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
394  Policy{a, +wi, +wa, +lw} = p
395  do Result<&1, &1, Err, Unit>:
396    exp : Maybe<&2, U32> <- when(field(c, "exp"))
397    nbf : Maybe<&2, U32> <- when(field(c, "nbf"))
398    iat : Maybe<&2, U32> <- when(field(c, "iat"))
399    gi : Maybe<&2, String> <- text(field(c, "iss"))
400    ga : Maybe<&2, List<&2, String>> <- auds(field(c, "aud"))
401    u1 : Unit <- fail.if(late(now, lw, exp), Expired{})
402    u2 : Unit <- fail.if(early(now, lw, nbf), NotYet{})
403    u3 : Unit <- fail.if(early(now, lw, iat), Future{})
404    u4 : Unit <- fail.if(iss.bad(wi, gi), BadIss{})
405    fail.if(aud.bad(wa, ga), BadAud{})
406
407def inspect.parts(+p: Policy, +now: U32, r: Result<&1, &1, Err, Parts>) -> Result<&1, &1, Err, Unit>:
408  match r:
409    case Fail{e}:
410      Fail{e}
411    case Done{Parts{+h, +f, v, input, sig}}:
412      do Result<&1, &1, Err, Unit>:
413        u : Unit <- head.check(policy.alg(p), h)
414        claims.check(p, now, f)
415
416# The header and claims of token, without its signature: the pure half of verify.
417def inspect(p: Policy, token: String, +now: U32) -> Result<&1, &1, Err, Unit>:
418  inspect.parts(p, now, parse(token))
419
420# ---- signatures
421
422def crypto.bytes(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, Err, Bytes.Bytes>:
423  match r:
424    case Fail{(c, w)}:
425      Fail{Crypto{c, w}}
426    case Done{(n, b)}:
427      Done{Bytes.Bytes{n, b}}
428
429def crypto.ok(r: Result<&1, &1, U32 & String, Bool>) -> Result<&1, &1, Err, Bool>:
430  match r:
431    case Fail{(c, w)}:
432      Fail{Crypto{c, w}}
433    case Done{b}:
434      Done{b}
435
436def mac.if(weak: Bool, +alg: String, +kn: U32, kb: Array<U32>, +dn: U32, db: Array<U32>) ->
437    IO(Result<&1, &1, Err, Bytes.Bytes>):
438  match weak:
439    case True{}:
440      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{WeakKey{}})
441    case False{}:
442      do IO<Result<&1, &1, Err, Bytes.Bytes>>:
443        r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.hmac.words(alg, kn, kb, dn, db)
444        return crypto.bytes(r)
445
446def mac(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
447  Bytes.Bytes{+kn, kb} = k
448  Bytes.Bytes{+dn, db} = input
449  mac.if(U32.is_lt(kn, min), alg, kn, kb, dn, db)
450
451def mac.cmp(m: Result<&1, &1, Err, Bytes.Bytes>, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
452  match m:
453    case Fail{e}:
454      IO.pure(Result<&1, &1, Err, Bool>, Fail{e})
455    case Done{Bytes.Bytes{+mn, mb}}:
456      Bytes.Bytes{+sn, sb} = sig
457      do IO<Result<&1, &1, Err, Bool>>:
458        ok : Bool <- Crypto.eq.ct.words(mn, mb, sn, sb)
459        return Done{ok}
460
461# The MAC compares in constant time.
462def mac.check(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
463  do IO<Result<&1, &1, Err, Bool>>:
464    m : Result<&1, &1, Err, Bytes.Bytes> <- mac(alg, min, k, input)
465    mac.cmp(m, sig)
466
467def rsa.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
468  Bytes.Bytes{+pn, pb} = p
469  Bytes.Bytes{+dn, db} = input
470  Bytes.Bytes{+sn, sb} = sig
471  do IO<Result<&1, &1, Err, Bool>>:
472    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
473    return crypto.ok(r)
474
475def rsa.jwk(n: Bytes.Bytes, e: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
476  Bytes.Bytes{+nn, nb} = n
477  Bytes.Bytes{+en, eb} = e
478  Bytes.Bytes{+dn, db} = input
479  Bytes.Bytes{+sn, sb} = sig
480  do IO<Result<&1, &1, Err, Bool>>:
481    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.jwk.words("SHA256", nn, nb, en, eb, dn, db, sn, sb)
482    return crypto.ok(r)
483
484def ec.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
485  Bytes.Bytes{+pn, pb} = p
486  Bytes.Bytes{+dn, db} = input
487  Bytes.Bytes{+sn, sb} = sig
488  do IO<Result<&1, &1, Err, Bool>>:
489    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
490    return crypto.ok(r)
491
492def ec.jwk(x: Bytes.Bytes, y: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
493  Bytes.Bytes{+xn, xb} = x
494  Bytes.Bytes{+yn, yb} = y
495  Bytes.Bytes{+dn, db} = input
496  Bytes.Bytes{+sn, sb} = sig
497  do IO<Result<&1, &1, Err, Bool>>:
498    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.jwk.words("SHA256", xn, xb, yn, yb, dn, db, sn, sb)
499    return crypto.ok(r)
500
501# Does sig sign input under key for alg? A key of the wrong kind fails with KeyType before any crypto.
502def sig.check(a: Alg, key: Key, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
503  match a key:
504    case HS256{} Hmac{k}:
505      mac.check("SHA256", 32, k, input, sig)
506    case HS384{} Hmac{k}:
507      mac.check("SHA384", 48, k, input, sig)
508    case HS512{} Hmac{k}:
509      mac.check("SHA512", 64, k, input, sig)
510    case RS256{} Pem{p}:
511      rsa.pem(p, input, sig)
512    case RS256{} Rsa{n, e}:
513      rsa.jwk(n, e, input, sig)
514    case ES256{} Pem{p}:
515      ec.pem(p, input, sig)
516    case ES256{} Ec{x, y}:
517      ec.jwk(x, y, input, sig)
518    case _ _:
519      IO.pure(Result<&1, &1, Err, Bool>, Fail{KeyType{}})
520
521def rsa.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
522  Bytes.Bytes{+pn, pb} = p
523  Bytes.Bytes{+dn, db} = input
524  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
525    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.rsa.sign.words("SHA256", pn, pb, dn, db)
526    return crypto.bytes(r)
527
528def ec.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
529  Bytes.Bytes{+pn, pb} = p
530  Bytes.Bytes{+dn, db} = input
531  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
532    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.ecdsa.sign.words("SHA256", pn, pb, dn, db)
533    return crypto.bytes(r)
534
535# The signature of input under key for alg. RS256 and ES256 sign with a PEM private key.
536def sig.make(a: Alg, key: Key, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
537  match a key:
538    case HS256{} Hmac{k}:
539      mac("SHA256", 32, k, input)
540    case HS384{} Hmac{k}:
541      mac("SHA384", 48, k, input)
542    case HS512{} Hmac{k}:
543      mac("SHA512", 64, k, input)
544    case RS256{} Pem{p}:
545      rsa.sign(p, input)
546    case ES256{} Pem{p}:
547      ec.sign(p, input)
548    case _ _:
549      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{KeyType{}})
550
551# ---- sign and verify
552
553def header.kid(m: Maybe<&2, String>) -> List<&1, Bytes.Bytes & Json.Val>:
554  match m:
555    case None{}:
556      Nil{}
557    case Some{k}:
558      [(Json.utf8("kid"), Json.Str{Json.utf8(k)})]
559
560# {"alg":..,"typ":"JWT"}, then "kid" when given.
561def header(a: Alg, kid: Maybe<&2, String>) -> Json.Val:
562  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)}}}
563
564# header.body in base64url, body being the compact JSON claims: the text the signature covers.
565def signing.input(a: Alg, kid: Maybe<&2, String>, body: Bytes.Bytes) -> String:
566  b64u(Json.encode.bytes(header(a, kid))) ++ "." ++ b64u(body)
567
568def sign.done(+input: String, s: Result<&1, &1, Err, Bytes.Bytes>) -> Result<&1, &1, Err, String>:
569  match s:
570    case Fail{e}:
571      Fail{e}
572    case Done{b}:
573      Done{input ++ "." ++ b64u(b)}
574
575# verify accepts only an object with no repeated names, so sign makes no other kind.
576def sign.obj(m: Maybe<&1, Json.Val>) -> Bool:
577  match m:
578    case Some{Json.Obj{kvs}}:
579      True{}
580    case _:
581      False{}
582
583def sign.if(ok: Bool, +a: Alg, key: Key, kid: Maybe<&2, String>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
584  match ok:
585    case False{}:
586      IO.pure(Result<&1, &1, Err, String>, Fail{BadClaim{}})
587    case True{}:
588      +input = signing.input(a, kid, body)
589      do IO<Result<&1, &1, Err, String>>:
590        s : Result<&1, &1, Err, Bytes.Bytes> <- sig.make(a, key, Bytes.from_string(input))
591        return sign.done(input, s)
592
593def sign.body(+a: Alg, key: Key, kid: Maybe<&2, String>, r: Bytes.Bytes & Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
594  (body, copy) = r
595  sign.if(sign.obj(Json.unique.parsed(Json.parse.bytes(copy))), a, key, kid, body)
596
597# A compact token of claims signed with key for a; kid names the key in the header. Claims that are not
598# an object, or repeat a name, fail with BadClaim.
599def sign(+a: Alg, key: Key, kid: Maybe<&2, String>, claims: Json.Val) -> IO(Result<&1, &1, Err, String>):
600  sign.body(a, key, kid, Bytes.slice(Json.encode.bytes(claims), 0, 4294967295))
601
602def claims.done(r: Result<&1, &1, Err, Unit>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
603  match r:
604    case Fail{e}:
605      Fail{e}
606    case Done{u}:
607      Done{v}
608
609def check.sig(ok: Bool, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
610  match ok:
611    case False{}:
612      Fail{BadSig{}}
613    case True{}:
614      claims.done(claims.check(p, now, f), v)
615
616def check.done(s: Result<&1, &1, Err, Bool>, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) ->
617    Result<&1, &1, Err, Json.Val>:
618  match s:
619    case Fail{e}:
620      Fail{e}
621    case Done{ok}:
622      check.sig(ok, p, now, f, v)
623
624def check.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, key: Key, +now: U32, +f: List<&2, Field>, v: Json.Val,
625    input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Json.Val>):
626  match ok:
627    case Fail{e}:
628      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
629    case Done{u}:
630      do IO<Result<&1, &1, Err, Json.Val>>:
631        s : Result<&1, &1, Err, Bool> <- sig.check(policy.alg(p), key, input, sig)
632        return check.done(s, p, now, f, v)
633
634# The pinned alg, then the signature, then the claims.
635def check(+p: Policy, key: Key, +now: U32, parts: Parts) -> IO(Result<&1, &1, Err, Json.Val>):
636  Parts{+h, +f, v, input, sig} = parts
637  check.pinned(head.check(policy.alg(p), h), p, key, now, f, v, input, sig)
638
639def verify.parsed(+p: Policy, key: Key, +now: U32, r: Result<&1, &1, Err, Parts>) -> IO(Result<&1, &1, Err, Json.Val>):
640  match r:
641    case Fail{e}:
642      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
643    case Done{parts}:
644      check(p, key, now, parts)
645
646# The claims of token when it is signed by key under p's alg and its claims hold at unix time now.
647def verify(+p: Policy, key: Key, token: String, +now: U32) -> IO(Result<&1, &1, Err, Json.Val>):
648  verify.parsed(p, key, now, parse(token))
649
650# ---- JWKS (RFC 7517)
651
652# A usable public key from a set: its kid, RSA or EC P-256, its alg ("" when the set gives none), and its
653# two base64url parts (n and e, or x and y).
654type Jwk is Data:
655  Jwk{kid: String, rsa: Bool, alg: String, a: String, b: String}
656
657def jwk.two(+rsa: Bool, +kid: String, +alg: String, a: Maybe<&2, String>, b: Maybe<&2, String>) -> Maybe<&2, Jwk>:
658  match a b:
659    case Some{x} Some{y}:
660      Some{Jwk{kid, rsa, alg, x, y}}
661    case _ _:
662      None{}
663
664# An alg member that is not a string can match no pinned alg.
665def jwk.alg(m: Maybe<&2, Lit>) -> String:
666  match m:
667    case None{}:
668      ""
669    case Some{LStr{s}}:
670      s
671    case Some{_}:
672      "?"
673
674def jwk.use(m: Maybe<&2, Lit>) -> Maybe<&2, Unit>:
675  match m:
676    case None{}:
677      Some{Unit{}}
678    case Some{LStr{s}}:
679      Bool.pick(Maybe<&2, Unit>, String.eq(s, "sig"), Some{Unit{}}, None{})
680    case Some{_}:
681      None{}
682
683def jwk.kty(+kty: String, +kid: String, +f: List<&2, Field>) -> Maybe<&2, Jwk>:
684  +alg = jwk.alg(field(f, "alg"))
685  +ec = Bool.and(String.eq(kty, "EC"), String.eq(Maybe.default(&2, String, str(field(f, "crv")), ""), "P-256"))
686  Bool.pick(Maybe<&2, Jwk>, String.eq(kty, "RSA"), jwk.two(True{}, kid, alg, str(field(f, "n")), str(field(f, "e"))),
687    Bool.pick(Maybe<&2, Jwk>, ec, jwk.two(False{}, kid, alg, str(field(f, "x")), str(field(f, "y"))), None{}))
688
689def jwk.fields(+f: List<&2, Field>) -> Maybe<&2, Jwk>:
690  do Maybe<&2, Jwk>:
691    kty : String <- str(field(f, "kty"))
692    kid : String <- str(field(f, "kid"))
693    s : Unit <- jwk.use(field(f, "use"))
694    jwk.kty(kty, kid, f)
695
696def jwk.obj(m: Maybe<&1, Json.Val>) -> Maybe<&2, Jwk>:
697  match m:
698    case Some{Json.Obj{kvs}}:
699      jwk.fields(fields(kvs, Nil{}))
700    case _:
701      None{}
702
703# A key whose members repeat a name, at any depth, is skipped.
704def jwk.of(v: Json.Val) -> Maybe<&2, Jwk>:
705  jwk.obj(Json.unique.parsed(Some{v}))
706
707def jwk.push(m: Maybe<&2, Jwk>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
708  match m:
709    case None{}:
710      acc
711    case Some{k}:
712      Con{k, acc}
713
714def jwks.go(xs: List<&1, Json.Val>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
715  match xs:
716    case Nil{}:
717      List.reverse(&2, Jwk, acc)
718    case x <> t:
719      jwks.go(t, jwk.push(jwk.of(x), acc))
720
721def jwks.arr(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
722  match m:
723    case Some{Json.Arr{xs}}:
724      Some{jwks.go(xs, Nil{})}
725    case _:
726      None{}
727
728def jwks.doc(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
729  match m:
730    case Some{v}:
731      jwks.arr(Json.get(v, "keys"))
732    case None{}:
733      None{}
734
735# The signing keys of a JWK Set document; members it cannot use (enc keys, other curves, oct) are skipped.
736# None when the document is not {"keys": [...]}.
737def jwks.parse(b: Bytes.Bytes) -> Maybe<&2, List<&2, Jwk>>:
738  jwks.doc(Json.parse.bytes(b))
739
740def fam(a: Alg) -> U32:
741  match a:
742    case RS256{}:
743      1
744    case ES256{}:
745      2
746    case _:
747      0
748
749def jwk.fits(k: Jwk, +kid: String, +a: Alg) -> Bool:
750  Jwk{k2, +rsa, +ka, x, y} = k
751  Bool.and(Bool.and(String.eq(k2, kid), U32.is_eq(fam(a), Bool.pick(U32, rsa, 1, 2))),
752    Bool.or(String.eq(ka, ""), String.eq(ka, alg.name(a))))
753
754# The first key named kid that can check alg a. RFC 7515 §4.1.4 leaves kid matching to exact comparison.
755def jwk.pick(ks: List<&2, Jwk>, +kid: String, +a: Alg) -> Maybe<&2, Jwk>:
756  match ks:
757    case Nil{}:
758      None{}
759    case Con{+k, t}:
760      Bool.pick(Maybe<&2, Jwk>, jwk.fits(k, kid, a), Some{k}, jwk.pick(t, kid, a))
761
762def jwk.key.of(rsa: Bool, a: Maybe<&1, Bytes.Bytes>, b: Maybe<&1, Bytes.Bytes>) -> Result<&1, &1, Err, Key>:
763  match rsa a b:
764    case True{} Some{n} Some{e}:
765      Done{Rsa{n, e}}
766    case False{} Some{x} Some{y}:
767      Done{Ec{x, y}}
768    case _ _ _:
769      Fail{Malformed{}}
770
771# A set member as a verify key.
772def jwk.key(k: Jwk) -> Result<&1, &1, Err, Key>:
773  Jwk{kid, +rsa, alg, +a, +b} = k
774  jwk.key.of(rsa, unb64u(a), unb64u(b))
775
776def jwk.found(m: Maybe<&2, Jwk>) -> Result<&1, &1, Err, Key>:
777  match m:
778    case None{}:
779      Fail{NoKey{}}
780    case Some{k}:
781      jwk.key(k)
782
783# A cached key set from the caller's own trusted url; a token never picks the url (jku and x5u are ignored).
784# live: fetched once; at: the unix time of the last good fetch; ttl: seconds it stays fresh;
785# tried: the unix time of the last fetch, good or not.
786type Jwks is Data:
787  Jwks{url: String, ttl: U32, live: Bool, at: U32, tried: Maybe<&2, U32>, keys: List<&2, Jwk>}
788
789def jwks(url: String, +ttl: U32) -> Jwks:
790  Jwks{url, ttl, False{}, 0, None{}, Nil{}}
791
792def jwks.keys(s: Jwks) -> List<&2, Jwk>:
793  Jwks{u, t, l, a, tr, ks} = s
794  ks
795
796def fetch.keys(m: Maybe<&2, List<&2, Jwk>>, c: Hairpin.Client, s: Jwks, +now: U32) -> Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
797  match m:
798    case None{}:
799      (c, s, Fail{Malformed{}})
800    case Some{ks}:
801      Jwks{url, ttl, live, at, tried, old} = s
802      (c, Jwks{url, ttl, True{}, now, tried, ks}, Done{Unit{}})
803
804def fetch.body(ok: Bool, +status: U32, c: Hairpin.Client, s: Jwks, +now: U32, b: Bytes.Bytes) ->
805    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
806  match ok:
807    case False{}:
808      (c, s, Fail{Status{status}})
809    case True{}:
810      fetch.keys(jwks.parse(b), c, s, now)
811
812def fetch.res(c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Hairpin.Err, Http.Res>) ->
813    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
814  match r:
815    case Fail{e}:
816      (c, s, Fail{Net{e}})
817    case Done{Http.Res{+status, h, b}}:
818      fetch.body(U32.is_eq(status, 200), status, c, s, now, b)
819
820def fetch.done(s: Jwks, +now: U32, x: Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res>) ->
821    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
822  (c, r) = x
823  fetch.res(c, s, now, r)
824
825# GET the set now. On any failure the client and the old keys come back, with only tried moved to now.
826def fetch(c: Hairpin.Client, s: Jwks, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>):
827  Jwks{+url, ttl, live, at, old, ks} = s
828  do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>>:
829    x : Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res> <- Hairpin.get(c, url)
830    return fetch.done(Jwks{url, ttl, live, at, Some{now}, ks}, now, x)
831
832def key.after.r(r: Result<&1, &1, Err, Unit>, c: Hairpin.Client, +s: Jwks, +kid: String, +a: Alg) ->
833    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
834  match r:
835    case Fail{e}:
836      (c, s, Fail{e})
837    case Done{u}:
838      (c, s, jwk.found(jwk.pick(jwks.keys(s), kid, a)))
839
840def key.after(+kid: String, +a: Alg, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>) ->
841    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
842  (c, s, r) = x
843  key.after.r(r, c, s, kid, a)
844
845def key.refetch(go: Bool, c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) ->
846    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
847  match go:
848    case False{}:
849      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, Fail{NoKey{}}))
850    case True{}:
851      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Key>>:
852        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Unit> <- fetch(c, s, now)
853        return key.after(kid, a, x)
854
855def key.go(cached: Bool, +go: Bool, c: Hairpin.Client, s: Jwks, found: Maybe<&2, Jwk>, +kid: String, +a: Alg, +now: U32) ->
856    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
857  match cached:
858    case True{}:
859      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, jwk.found(found)))
860    case False{}:
861      key.refetch(go, c, s, kid, a, now)
862
863def since(+now: U32, m: Maybe<&2, U32>) -> U32:
864  match m:
865    case None{}:
866      4294967295
867    case Some{+t}:
868      Bool.pick(U32, U32.is_le(t, now), (now - t : U32), 0)
869
870# The verify key named kid for alg a. A known key stays usable through the 60 s fetch cooldown even
871# when ttl is shorter. After that, refresh a stale set or an unknown kid at most once a minute.
872# ponytail: fixed 60 s cooldown; make it a Jwks field if an issuer rotates faster.
873def key(c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
874  Jwks{+url, +ttl, +live, +at, +tried, +ks} = s
875  +found = jwk.pick(ks, kid, a)
876  +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))))
877  +cached = Bool.and(fresh, Maybe.is_some(&2, Jwk, found))
878  key.go(cached, U32.is_le(60, since(now, tried)), c, Jwks{url, ttl, live, at, tried, ks}, found, kid, a, now)
879
880def jwks.run(r: Result<&1, &1, Err, Key>, c: Hairpin.Client, s: Jwks, +p: Policy, +now: U32, parts: Parts) ->
881    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
882  match r:
883    case Fail{e}:
884      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
885    case Done{k}:
886      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
887        v : Result<&1, &1, Err, Json.Val> <- check(p, k, now, parts)
888        return (c, s, v)
889
890def jwks.keyed(+p: Policy, +now: U32, parts: Parts, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Key>) ->
891    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
892  (c, s, r) = x
893  jwks.run(r, c, s, p, now, parts)
894
895def jwks.kid(k: Maybe<&2, String>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, parts: Parts) ->
896    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
897  match k:
898    case None{}:
899      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{NoKey{}}))
900    case Some{+kid}:
901      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
902        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Key> <- key(c, s, kid, policy.alg(p), now)
903        jwks.keyed(p, now, parts, x)
904
905def jwks.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, +h: List<&2, Field>,
906    parts: Parts) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
907  match ok:
908    case Fail{e}:
909      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
910    case Done{u}:
911      jwks.kid(str(field(h, "kid")), p, c, s, now, parts)
912
913def jwks.parsed(+p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Err, Parts>) ->
914    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
915  match r:
916    case Fail{e}:
917      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
918    case Done{Parts{+h, f, v, input, sig}}:
919      jwks.pinned(head.check(policy.alg(p), h), p, c, s, now, h, Parts{h, f, v, input, sig})
920
921# verify with the key the token's kid names in the set. The alg is pinned before any fetch.
922# The client and the set (refreshed or not) always come back.
923def verify.jwks(+p: Policy, c: Hairpin.Client, s: Jwks, token: String, +now: U32) ->
924    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
925  jwks.parsed(p, c, s, now, parse(token))