Hale.Jose.Crypto.JOSE.Types

rsa (n e : ByteArray) (d : Option ByteArray) : JWKKeyMaterial
RSA public key: modulus n, exponent e, optional private exponent d.
ec (crv : ECCurve) (x y : ByteArray) (d : Option ByteArray) : JWKKeyMaterial
EC public key: curve, x-coordinate, y-coordinate, optional private key d.
oct (k : ByteArray) : JWKKeyMaterial
Symmetric (octet) key.

Instances For

source

def Crypto.JOSE.instReprJWKKeyMaterial.repr :

JWKKeyMaterial → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWKKeyMaterial :

Repr JWKKeyMaterial

Equations

Crypto.JOSE.instReprJWKKeyMaterial = { reprPrec := Crypto.JOSE.instReprJWKKeyMaterial.repr }

source

inductive Crypto.JOSE.JWKKeyType :

Type

Valid JWK key types per RFC 7518 §6.1.

Instances For

source

def Crypto.JOSE.instBEqJWKKeyType.beq :

JWKKeyType → JWKKeyType → Bool

Equations

Crypto.JOSE.instBEqJWKKeyType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instBEqJWKKeyType :

BEq JWKKeyType

Equations

Crypto.JOSE.instBEqJWKKeyType = { beq := Crypto.JOSE.instBEqJWKKeyType.beq }

source

@[implicit_reducible]

instance Crypto.JOSE.instDecidableEqJWKKeyType :

DecidableEq JWKKeyType

Equations

Crypto.JOSE.instDecidableEqJWKKeyType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWKKeyType :

Repr JWKKeyType

Equations

Crypto.JOSE.instReprJWKKeyType = { reprPrec := Crypto.JOSE.instReprJWKKeyType.repr }

source

def Crypto.JOSE.instReprJWKKeyType.repr :

JWKKeyType → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Crypto.JOSE.instInhabitedJWKKeyType.default :

JWKKeyType

Equations

Crypto.JOSE.instInhabitedJWKKeyType.default = Crypto.JOSE.JWKKeyType.RSA

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instInhabitedJWKKeyType :

Inhabited JWKKeyType

Equations

Crypto.JOSE.instInhabitedJWKKeyType = { default := Crypto.JOSE.instInhabitedJWKKeyType.default }

source

@[implicit_reducible]

instance Crypto.JOSE.instToStringJWKKeyType :

ToString JWKKeyType

Equations

One or more equations did not get rendered due to their size.

source

def Crypto.JOSE.JWKKeyType.fromString :

String → Option JWKKeyType

Parse a key type string.

Equations

Instances For

source

theorem Crypto.JOSE.JWKKeyType.fromString_toString_roundtrip (k : JWKKeyType) :

fromString (toString k) = some k

Roundtrip: fromString (toString k) = some k for all key types.

source

inductive Crypto.JOSE.JWKUse :

Type

Valid JWK public key usage values per RFC 7517 §4.2.

sig : JWKUse
enc : JWKUse

Instances For

source

def Crypto.JOSE.instBEqJWKUse.beq :

JWKUse → JWKUse → Bool

Equations

Crypto.JOSE.instBEqJWKUse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instBEqJWKUse :

BEq JWKUse

Equations

Crypto.JOSE.instBEqJWKUse = { beq := Crypto.JOSE.instBEqJWKUse.beq }

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWKUse :

Repr JWKUse

Equations

Crypto.JOSE.instReprJWKUse = { reprPrec := Crypto.JOSE.instReprJWKUse.repr }

source

def Crypto.JOSE.instReprJWKUse.repr :

JWKUse → Nat → Std.Format

Equations

Crypto.JOSE.instReprJWKUse.repr Crypto.JOSE.JWKUse.sig prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Crypto.JOSE.JWKUse.sig")).group prec✝
Crypto.JOSE.instReprJWKUse.repr Crypto.JOSE.JWKUse.enc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Crypto.JOSE.JWKUse.enc")).group prec✝

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instToStringJWKUse :

ToString JWKUse

Equations

Crypto.JOSE.instToStringJWKUse = { toString := fun (x : Crypto.JOSE.JWKUse) => match x with | Crypto.JOSE.JWKUse.sig => "sig" | Crypto.JOSE.JWKUse.enc => "enc" }

source

structure Crypto.JOSE.JWK :

Type

A JSON Web Key (RFC 7517). $$\text{JWK} = \{ \text{kty}, \text{kid}?, \text{alg}?, \text{use}?, \text{material} \}$$

The kty field is a JWKKeyType (not a raw String), constraining it to the valid values "RSA", "EC", "oct" per RFC 7518 §6.1. The kty_material_coherent proof ensures the key type matches the key material.

kty : JWKKeyType
Key type: constrained to valid values per RFC 7518 §6.1.
kid : Option String
Key ID (optional).
alg : Option JWSAlgorithm
Algorithm (optional).
use : Option JWKUse
Public key use: "sig" or "enc" (optional), now typed.
material : JWKKeyMaterial
The key material.
kty_material_coherent : (self.kty = JWKKeyType.RSA → ∃ (n : ByteArray ), ∃ (e : ByteArray ), ∃ (d : Option ByteArray), self.material = JWKKeyMaterial.rsa n e d) ∧ (self.kty = JWKKeyType.EC → ∃ (crv : ECCurve ), ∃ (x : ByteArray ), ∃ (y : ByteArray ), ∃ (d : Option ByteArray), self.material = JWKKeyMaterial.ec crv x y d) ∧ (self.kty = JWKKeyType.oct → ∃ (k : ByteArray ), self.material = JWKKeyMaterial.oct k)
The key type must be coherent with the key material.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWK :

Repr JWK

Equations

One or more equations did not get rendered due to their size.

source

structure Crypto.JOSE.JWKSet :

Type

A set of JWKs (RFC 7517 §5).

keys : Array JWK

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWKSet :

Repr JWKSet

Equations

Crypto.JOSE.instReprJWKSet = { reprPrec := fun (s : Crypto.JOSE.JWKSet) (x : Nat) => Std.Format.text (toString "JWKSet(keys=" ++ toString (repr s.keys) ++ toString ")") }

source

structure Crypto.JOSE.ClaimsSet :

Type

Registered claim names for JWTs (RFC 7519 §4.1).

iss : Option String
Issuer claim.
sub : Option String
Subject claim.
aud : Option (List String)
Audience claim (can be a single string or array).
exp : Option Nat
Expiration time (Unix timestamp).
nbf : Option Nat
Not before (Unix timestamp).
iat : Option Nat
Issued at (Unix timestamp).
jti : Option String
JWT ID.
unregisteredClaims : List (String × String)
Unregistered (custom) claims as key-value pairs. Values are stored as their JSON string representation.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprClaimsSet :

Repr ClaimsSet

Equations

Crypto.JOSE.instReprClaimsSet = { reprPrec := Crypto.JOSE.instReprClaimsSet.repr }

source

def Crypto.JOSE.instReprClaimsSet.repr :

ClaimsSet → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instInhabitedClaimsSet :

Inhabited ClaimsSet

Equations

Crypto.JOSE.instInhabitedClaimsSet = { default := Crypto.JOSE.instInhabitedClaimsSet.default }

source

def Crypto.JOSE.instInhabitedClaimsSet.default :

ClaimsSet

Equations

Crypto.JOSE.instInhabitedClaimsSet.default = { iss := default, sub := default, aud := default, exp := default, nbf := default, iat := default, jti := default, unregisteredClaims := default }

Instances For

source

def Crypto.JOSE.ClaimsSet.lookupClaim (claims : ClaimsSet) (key : String) :

Option String

Look up a custom claim value by name.

Equations

claims.lookupClaim key = List.lookup key claims.unregisteredClaims

Instances For

source

structure Crypto.JOSE.JWSHeader :

Type

JWS JOSE Header (RFC 7515 §4).

Instances For

source

def Crypto.JOSE.instBEqJWSHeader.beq :

JWSHeader → JWSHeader → Bool

Equations

Crypto.JOSE.instBEqJWSHeader.beq { alg := a, kid := a_1, typ := a_2, cty := a_3 } { alg := b, kid := b_1, typ := b_2, cty := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
Crypto.JOSE.instBEqJWSHeader.beq x✝¹ x✝ = false

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instBEqJWSHeader :

BEq JWSHeader

Equations

Crypto.JOSE.instBEqJWSHeader = { beq := Crypto.JOSE.instBEqJWSHeader.beq }

source

def Crypto.JOSE.instReprJWSHeader.repr :

JWSHeader → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWSHeader :

Repr JWSHeader

Equations

Crypto.JOSE.instReprJWSHeader = { reprPrec := Crypto.JOSE.instReprJWSHeader.repr }

source

structure Crypto.JOSE.JWTValidationSettings :

Type

Configuration for JWT validation. allowedSkew is bounded to at most 600 seconds (10 minutes) to prevent dangerously permissive clock skew that could accept expired/future tokens.

allowedSkew : Nat
Allowed clock skew in seconds (max 600 = 10 minutes).
allowedSkew_bounded : self.allowedSkew ≤ 600
The clock skew must not exceed 10 minutes (600 seconds).
checkExpiry : Bool
Whether to check the exp claim.
checkNotBefore : Bool
Whether to check the nbf claim.
audienceMatches : Option (List String)
If set, the aud claim must contain one of these values.
issuerMatches : Option (List String)
If set, the iss claim must be one of these values.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instReprJWTValidationSettings :

Repr JWTValidationSettings

Equations

Crypto.JOSE.instReprJWTValidationSettings = { reprPrec := Crypto.JOSE.instReprJWTValidationSettings.repr }

source

def Crypto.JOSE.instReprJWTValidationSettings.repr :

JWTValidationSettings → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Crypto.JOSE.instInhabitedJWTValidationSettings :

Inhabited JWTValidationSettings

Equations

Crypto.JOSE.instInhabitedJWTValidationSettings = { default := { allowedSkew_bounded := Crypto.JOSE.instInhabitedJWTValidationSettings._proof_2 } }

source

inductive Crypto.JOSE.JwtError :

Type

Errors that can occur during JWT validation.

malformedToken (msg : String) : JwtError
The JWT string has an invalid format (not 3 dot-separated parts).
headerParseError (msg : String) : JwtError
The header JSON cannot be parsed.
claimsParseError (msg : String) : JwtError
The claims JSON cannot be parsed.
unsupportedAlgorithm (alg : String) : JwtError
The algorithm in the header is not supported.
signatureVerificationFailed : JwtError
Signature verification failed.
tokenExpired (exp now : Nat) : JwtError
The token has expired.
tokenNotYetValid (nbf now : Nat) : JwtError
The token is not yet valid.
audienceMismatch : JwtError
The audience claim does not match.
issuerMismatch : JwtError
The issuer claim does not match.
noMatchingKey : JwtError
No matching key found in the key set.
noneAlgorithmNotAllowed : JwtError
The "none" algorithm is not allowed.