def Crypto.JOSE.JWT.validateClaims (claims : ClaimsSet) (now : Nat) (settings : JWTValidationSettings) : Except JwtError Unit

Validate registered JWT claims against the current time and settings.

Equations

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

def Crypto.JOSE.JWT.verifyJWT (token : String) (keySet : JWKSet) (now : Nat) (settings : JWTValidationSettings := { allowedSkew_bounded := ⋯ }) : IO (Except JwtError ClaimsSet)

Verify and decode a JWT token. Returns the validated claims set on success.

Equations

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

def Crypto.JOSE.JWT.verifyJWT.extractJsonField (json key : String) : Option String

Extract a JSON string field value (very simplified parser). Uses String.splitOn to locate patterns, avoiding raw String.Pos manipulation.

Equations

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

def Crypto.JOSE.JWT.verifyJWT.extractAllFields (_json : String) : List (String × String)

Extract all key-value pairs from a simple JSON object.

Equations

• Crypto.JOSE.JWT.verifyJWT.extractAllFields _json = []