Independent Implementation and Formal Analysis of Attenuating Delegation Chains for AI Agents

3.1. AAT-01 and AAT-02

[AAT-01] (Niyikiza) defines Attenuating Authorization Tokens: JWTs whose authorization_details ([RFC9396]) list the tools a holder may invoke and typed constraints on each argument. A root token is issued by a root issuer and verified under a configured trust anchor key. Each later token is derived offline by the holder of its parent: it is signed by the key the parent names in cnf.jwk, its iss is that key's JWK thumbprint URI ([RFC9278]), and its par_hash is the SHA-256 hash of the parent's JWS signing input (Section 4.6). The invariants I1 to I6 (Section 4) let a derived token only narrow tools, argument constraints (by a per-type subsumption relation, Section 4.5), delegation depth and lifetime. At each tool invocation the leaf holder presents a proof-of-possession (PoP) JWT over the tool and its arguments (Section 5); an enforcement point checks the chain and the proof in one algorithm (Section 7).¶

[AAT-02] (26 October 2026) keeps this structure and makes normative changes that, by its Appendix F, break -01 implementations. The JWS algorithm is the fully-specified Ed25519 ([RFC9864]) in place of EdDSA, and typ is required and explicit (aat+jwt for tokens, aat-pop+jwt for the PoP JWT). The PoP JWT carries aat_hash, the hash of the leaf's signing input. Trust anchors are (issuer, public key) pairs, and the root's iss must equal the issuer of the anchor whose key verified it. Parsing rules are strict: duplicate member names are rejected ([RFC8259]), NumericDates and depths have no fraction or exponent part, crit is processed, and numbers in arguments and constraints must be admissible (-02 Section 3.4). Constraint maps gain optional arguments and a "*" entry for arguments they do not name (-02 Section 3.3). The subsumption relation is written as a table of valid (parent, derived) pairs, every other pair invalid (-02 Section 4.5). MAX_DELEGATION_DEPTH is at least 8. A presentation object with members aat_chain and aat_pop is defined (-02 Section 7.4). The verification algorithm is -02 Section 8; this report names its steps by number and letter (for example, step 3k). -02 publishes a byte-exact JWS test-vector suite and lists implementations in its Appendix E. Both versions are implemented; the model is of -01 (see Section 5).¶

3.2. asor-02

[ASOR-02] (Asor) defines the Agent Delegation Chain, a profile of OAuth 2.0 JWT access tokens ([RFC9068]). Each Delegation Token carries its authority as authorization_details ([RFC9396]), the principal in sub (the same value in every token of the chain), the acting agent in client_id, a del_depth that grows by one per hop and is bounded by del_max_depth, and, below the root, a par_hash: the SHA-256 hash of the parent's JWS signing input. Tokens are verified under keys configured at the verifier (Section 6, step 1). The leaf is bound to its holder by cnf ([RFC7800]) and a DPoP proof ([RFC9449]). The offline verification algorithm (Section 6) enforces monotonic attenuation, bounded depth, monotonic expiry and the same principal throughout. Modelled and implemented.¶

5.1. Properties

For both profiles:¶

P1a:

Every root of a chain that passes the link checks was minted by the anchor.¶

P1b:

Every link whose parent names an honest holder key was derived from that parent by that holder, unless the key was compromised. For asor-02, the variant P1b' states the same with "some uncompromised configured key" in place of the parent's holder (see A7).¶

P2:

The invoked tool was granted at the root.¶

P3:

Leaf depth, maximum depth and expiry are bounded by the root's.¶

P4:

A leaf naming an honest key is used only by that key's holder (non-injective).¶

M1:

Parent validity after derivation: a parent is still accepted after its holder has derived a child from it, with no compromise at all.¶

M2:

Intermediate links carry no proof of possession of their own. Variants (a) an attacker derives a child of a token it merely observed, (b) a request is accepted under such a link, (c) a token is usable without its holder's key.¶

M1 and M2 are the two points of [MADDEN-REVIEW].¶

5.2. Results

Each row is one query of one model file. A file without a suffix is a profile with every check in place, and every query of it is expected true. A .expectfalse file is a variant with one check removed (no-i5, no-i6, nodpop) or asks for a property the profile does not claim (p4-inj, asor02-p1b, the asor-02 M2 files), and at least one of its queries is expected false; a .reachable file asks whether an event occurs in a run of honest roles only, and "reached" is the expected answer. A "false" in a variant is therefore the expected outcome of that variant, not a failed proof; each is accompanied by a ProVerif derivation and trace in model/out/, summarized in model/README.md. hs is the holder-signs flag of the asor-02 model (Section 8). A "true" is a ProVerif proof for an unbounded number of sessions of the bounded model (Section 5.3), not a statement about the draft text. Seconds are wall-clock per model file on one machine under make -j6, from model/out/SUMMARY.md; they are indicative.¶

5.3. What the Model Does Not Say

Nothing about constraint semantics below the tool level, time (freshness, skew, lifetimes; only expiry order), revocation, the trust anchor's key, size and algorithm checks, or chains longer than four tokens. A "true" is a ProVerif proof for unbounded sessions of the bounded model, not for the draft text.¶

6.1. Constraints (B1 to B8)

• B1 (Section 4.5): cross-type subsumption is an allow-list. Section 4.5 of -01 defines subsumption as a fixed list of per-type rules over (derived, parent) constraint-type pairs and declares every other pair invalid (-02 writes the same list as a table). The list leaves out some pairs whose narrowing is decidable from the values alone. For a composite parent the list loses nothing of its own: an exact under an any can be written as a one-clause any (see B2). Two pairs are lost outright: a one_of whose members all fall inside a parent range, and an exact under a not_one_of, have no equivalent in the parent's type. This implementation follows the list and rejects all of them. -02 keeps the pairs and names the choice: the verifier compares types, not values, so that every verifier gives the same verdict.¶

  -02: closed as design -- -02 Section 4.5 lists every valid (parent, derived) pair and says "Every other pair is invalid"; J.19.1, J.19.4 to J.19.7 and J.8.4 deny semantically narrower pairs, and their notes call this conservative by design.¶

• B2 (Section 4.5): non-composite child under a composite parent. Section 4.5 of -01 gives rules for all and any only against a parent of the same type, so a plain constraint under a composite parent falls under the closing sentence and is invalid. This implementation rejects it. Nothing is lost beyond B1, because the child can be written in the parent's type. Under an any, a one-clause any is valid when the child narrows one of the parent's clauses. Under an all, the child has to narrow every parent clause: -01 matches each parent clause to a distinct derived clause, so the child is repeated once per clause, while -02 lets one derived clause satisfy several. Each step goes through the pairs, so the rewrite fails exactly where a clause meets one of the two pairs of B1, and an all with more clauses meets them more often.¶

  -02: closed as design -- J.8.4 (range under all) and J.19.1 (exact under any) are denied; J.18.1 denies all under any.¶

• B3 (Section 4.5): empty composite constraints. Section 4.5 of -01 says only that a derived any must contain at least one clause. An empty all is satisfied by every value and an empty any by none, so an empty parent all grants the argument without limit and an empty parent any forbids it; -01 addresses neither. This implementation treats an empty clause list as malformed for both types, in either position.¶

  -02: closed -- -02 Section 4.5 makes an empty all or any invalid in both the parent and the derived position; it is denied at steps 3n and 4o (J.21.7, J.16.3).¶

• B4 (Section 4.5): range corner cases. Section 4.5 of -01 compares the bounds of a derived range with the parent's, one bound at a time. It does not say what a range that no number satisfies means (min greater than max, or equal bounds with an exclusive side), nor what an inclusivity flag without its bound means. This implementation applies the bound rules literally, which never widens authority. An empty derived range whose bounds lie inside the parent's is accepted and denies every value; one whose bounds lie outside is rejected, although an empty set narrows anything. Under an empty parent every derived range that passes the bound rules is itself empty. A flag without its bound has no effect. A verifier that rejects empty ranges as malformed therefore denies more than this one, never less, and neither grants anything the parent does not.¶

  -02: partly -- -02 Section 3.4 well-formedness requires min not greater than max and inclusivity flags only with their bound (J.8.6, J.8.21, J.8.24). An empty range with equal bounds and an exclusive side (min equal to max, min_inclusive false) is still well-formed.¶

• B5 (Section 3.4): value model and equality. -01 says only that exact.value is "any scalar" and must be equal "exactly"; it does not say whether null is a scalar, whether 1 equals "1" or 1.0, or what happens to a number a parser cannot hold exactly. This implementation takes string, number and boolean, compares by JCS, and refuses integers beyond 2^53-1 so that a constraint and the tool see the same value. That refusal covers integers only: a fraction such as 1.00000000000000001 is still read as 1.¶

  -02: closed -- exact.value may be a string, number, boolean or null, equality is by JCS, and the admissibility rule of -02 Section 3.4 replaces this implementation's refusal of integers above 2^53-1 (J.8.8 permit; J.8.7, J.8.10, J.8.14 deny).¶

• B6 (Section 3.4): arrays as sets. -01 does not say whether order or duplicates matter in the arrays of contains and subset, so two verifiers can disagree on the same argument. This implementation treats both arrays as sets.¶

  -02: closed -- -02 Section 3.4: contains and subset "treat their arrays as sets" (J.26.11, J.26.12).¶

• B7 (Section 3.4): unknown members of a core constraint type. -01 specifies what to do with an unknown constraint type and says that unknown top-level claims are ignored, but not what to do with an unknown member of a known type. Ignoring it would be unsafe: a misspelt bound such as maximum for max would leave the argument unbounded. This implementation rejects such a constraint as malformed.¶

  -02: closed -- well-formedness allows "no members other than" those of the type (J.21.12, maximum). The strict reading of -01 taken by this implementation is now the text.¶

• B8 (Sections 3.6.2, 4.5): key-set rule and tool omission. Under a non-empty constraint map -01 fixes the shape of an invocation: every named argument must be present and no other may appear. A derived token may drop a whole tool (Section 3.6.2) but must keep exactly the parent's argument keys, because adding or dropping a key yields invocations the parent would reject. The rules are consistent; the cost is rigidity. A holder cannot forbid one argument while keeping the tool, and an argument the issuer wants to leave optional cannot be constrained at all; only a parent with an empty map lets a child choose keys. This implementation follows the rules as written.¶

  -02: moot -- optional and "*" (-02 Section 3.3, the key rules of -02 Section 4.5, steps 4p2 and 4p3) give the means the closed-world key rule lacked (J.22.*).¶

6.2. Chain (B9 to B19)

• B9 (Section 4, Section 7): redundant checks (I2e, step 5). Some checks of -01 Section 7 follow from others. child.del_depth <= parent.del_max_depth (4e) follows from 4g and 4m, child.del_depth <= MAX_DELEGATION_DEPTH (4f) from 3i, 4g and 4m, and the "defense in depth" step 5 from 3c and 4d. No input fails one of them alone; this implementation keeps all of them, and its property tests reach 4e only together with 4g or 4m. Redundant checks are harmless, but a test suite cannot cover them as single faults.¶

  -02: open -- unchanged in -02 Section 8. The suite's README names "steps 4e, 4f and 5" among the checks that can never be the only fault. J.10.c reaches 4e only as the first of two faults (4m also fails).¶

• B10 (Section 4.4): MAX_TOKEN_LIFETIME is redundant by construction. A child cannot outlive its parent, so a lifetime bound checked on the root holds for every link; the note to step 4l of -01 says as much. This implementation checks it on every token anyway.¶

  -02: closed -- the notes to -02 Section 8 say the bound holds by induction (steps 3h, 4h and 4j); -02 has no per-child lifetime step.¶

• B11 (Section 7): which anchor key verifies the root and what iss means. In -01 the trust anchors are "a set of public keys" without issuer names; the root verifies under any of them (step 3b), and step 3k requires only that root.iss be a URI. Section 3.2 says that iss identifies the root issuer, but nothing ties it to the key that verified the signature. When an enforcement point trusts more than one issuer, any of them can sign a root that names another as iss, and the chain verifies. Within -01 this does not change a verdict, since nothing else reads root.iss; it matters as soon as audit or local policy relies on the issuer. The aat-01 profile follows -01 and accepts the root under any anchor; the aat-02 profile implements the new step 3k.¶

  -02: closed -- trust anchors are (issuer, key) pairs; step 3k compares the root's iss with the issuer of the anchor that verified the signature (J.21.6, J.21.22, J.21.23).¶

• B12 (Section 4.2): I1 comparison of a URN as a string. I1 requires child.iss to equal jwk_thumbprint_uri(parent.cnf.jwk), a URN. [RFC8141] makes parts of a URN case-insensitive, so "equals" can be read as a string or as a URN comparison. This implementation compares strings exactly; it computes the thumbprint for OKP keys only, with the member order of [RFC7638]. An exact comparison can only deny more, never less.¶

  -02: open -- step 4c still says "equals"; -02 says nothing about case-insensitive comparison of the URN ([RFC8141]). J.27.6 pins only the thumbprint members.¶

• B13 (Sections 3.2, 7, 8.13): algorithms and thumbprints. -01 Section 3.2 requires support for Ed25519, while Section 8.13 admits the DPoP algorithm list, including ES256 and RS256, and the closing note of Section 7 mentions Ed448; I1 would then need thumbprints for those key types as well. This implementation accepts only EdDSA with an OKP Ed25519 key and always refuses symmetric algorithms (Section 8.13).¶

  -02: closed -- the fully-specified Ed25519 ([RFC9864]); -02 forbids accepting EdDSA and requires alg to be consistent with the key's kty and crv (J.7.5, J.7.8, J.7.10, J.14.b).¶

• B14 (Section 7): parse before verify. -01 Section 7 forbids reading claims before the signature is verified, but step 4b needs the parent's parsed cnf.jwk, and step 2c lets jti be extracted first. This implementation checks the size limits (2a, 2b), parses every token, and then verifies. The verdict is the same either way; only the reported code for a forged malformed token differs (malformed rather than signature_invalid).¶

  -02: closed -- steps 3b, 4b and 7b fix the order per token. With pairs walked in order, the parent's cnf.jwk is parsed before the child's signature is needed. The aat-02 profile follows the order literally; aat-01 keeps parse-first.¶

• B15 (Sections 3.2, 3.4): sub. -01 Section 3.2 "intentionally omits" sub, and Section 3.4 says a token must not be rejected solely for claims outside those defined. Rejecting a token with sub is therefore not required, and arguably not allowed. This implementation rejects it by default and has an option to accept it.¶

  -02: open -- -02 still "intentionally omits the sub claim" and requires unrecognized top-level claims to be ignored. The aat-02 profile does not reject sub by default (rejectSub false). No vector carries sub (J.27.1 covers other unrecognized claims).¶

• B16 (Section 3.2): jti format. -01 says jti SHOULD be a UUIDv7 and, when a UUID is used, MUST be lowercase and hyphenated, but steps 3j and 4b1 check only for a non-empty string. This implementation accepts any non-empty string and rejects a UUID-shaped value with upper-case letters.¶

  -02: closed -- the notes to -02 Section 8 say the lowercase UUID form "binds producers and has no verification step". The aat-02 profile checks only for a non-empty string (aat-01 still rejects upper-case UUIDs).¶

• B17 (Section 7): limits without defaults. MAX_DELEGATION_DEPTH has no recommended value in -01; the other limits (MAX_IAT_SKEW 30 s, MAX_TOKEN_LIFETIME 90 days, MAX_CONSTRAINT_DEPTH 32, MAX_TOKEN_SIZE 64 KiB, MAX_STACK_SIZE 256 KiB) are RECOMMENDED. Whether a chain is valid then depends on local configuration, and a test vector has to state the limits it assumes. This implementation uses 16 for the depth.¶

  -02: closed -- MAX_DELEGATION_DEPTH is at least 8 (J.10.f, J.21.15, J.21.19); the suite states every parameter.¶

• B18 (Section 4.6): par_hash covers the signing input, not the signature. Two JWS with the same signing input and different signature bytes are therefore the same parent for I5. With Ed25519 and strict verification this cannot be exploited; the choice is still worth stating in the draft, since a profile with a malleable signature algorithm would inherit it.¶

  -02: open -- unchanged design; aat_hash is computed the same way.¶

• B19 (Sections 4.2, 4.7, 8.9): the review's points as AAT-01 answers them. [MADDEN-REVIEW], posted on the OAuth list the day -01 appeared, makes two technical points about the chain, apart from the comparison with HMAC-chained Macaroons and SPKI/SDSI: a parent token stays valid after a child has been derived from it, so the design lacks the re-keying of Macaroons; and only the leaf proves possession, so an agent that sees the bytes of an intermediate or root token could use them. The author's reply on the list called additive derivation intended and every token holder-bound. This report names the points M1 and M2 (Section 5.1) and checks them in the model rather than in the reply. The second point -01 answers in its text. Section 4.2 (I1) requires the derived token to be signed by the holder of the parent, Section 4.6 (I5) commits it to that parent's bytes, and Section 4.7 (I6) requires the presenter to prove possession of the leaf key. A token observed in transit can therefore neither be extended, since derivation needs its holder's key, nor presented as a leaf, nor moved under another parent. The model confirms this for -01: against an attacker who sees every token and may hold any holder key other than that of the token in question, no link is derived from it (M2 a, P1b), no request is accepted through such a link (M2 b), and no request is accepted with it (M2 c, P4). The first point -01 does not state. Nothing in the text says that a parent remains valid after derivation; Section 8.9 puts revocation out of scope and recommends short lifetimes, and Sections 8.1.2 and 8.4 give the consequence, that a compromised holder key exercises the full authority of every token bound to it until expiry, without the property behind it. The model shows M1 as a run of honest roles alone: a holder derives a child from its token and is then accepted with that same token, with no key compromised. It is how the design works, not an attack on it. This implementation checks I1, I5 and I6 and keeps no state that would retire a parent after derivation, since -01 defines none.¶

  -02: closed as design -- -02 Section 9.1.1 says that derivation is additive, that every token in a chain carries a holder key, and that a sub-agent holding its parent's bytes cannot invoke with them; -02 Section 9.4 says that AATs do not re-key, that a compromised holder key exposes every token bound to it, and gives deriving to a fresh key and destroying the parent's key as the approximation (-02 Section 9.4, with the fresh holder key of -02 Section 9.10). M1 and M2 (Section 5.1) are this report's independent check of it; the vectors do not bear on it.¶

6.3. Proof of Possession (B20 to B23)

• B20 (Section 5.2): PoP header and typ. -01 specifies no typ, kid or jwk header parameter for the PoP JWT, so nothing distinguishes it from another JWT signed by the same key. This implementation looks only at alg.¶

  -02: closed -- typ is aat-pop+jwt (J.7.1, J.7.2); a jwk header parameter is ignored as a key source (J.7.14).¶

• B21 (Sections 5.2, 7): JCS of the whole PoP payload. -01 Section 5.2 requires the holder to serialize the whole PoP payload with JCS, but step 7f compares only hta, and nothing says whether an enforcement point must reject a payload that is not canonical. This implementation rejects it: the payload bytes must equal their JCS re-serialization.¶

  -02: closed (requirement dropped) -- -02 Appendix F: "PoP payloads no longer need to be JCS-canonical". Only hta is compared (step 7f).¶

• B22 (Section 7): clock tolerance. -01 recommends a PoP window of 30 seconds either side, and separately a one-sided MAX_IAT_SKEW of 30 seconds for tokens; it does not say whether the two are the same parameter. This implementation keeps them apart: the PoP window is its own option, symmetric, with inclusive bounds.¶

  -02: closed -- -02 Section 9.9 separates the one-sided MAX_IAT_SKEW from the bilateral PoP window (J.20.4, J.20.15, J.20.16).¶

• B23 (Section 5): PoP binds the leaf only. In -01 the PoP JWT names the leaf by aat_id, which must equal the leaf's jti (Section 5.3), a value chosen by whoever derived the leaf; neither the leaf's bytes nor the chain enter the PoP signature. Which chain a PoP belongs to therefore rests on jti being unique across derivers, which nothing checks (steps 3j and 4b1 accept any non-empty string), and aat_aud is optional. The model shows the consequence: one PoP signed by an honest holder is accepted under two different chains that end in leaves with that holder's key and that jti (trace aat01-p4-inj, Section 5.2). This implementation compares aat_id with the leaf jti, as -01 says, and nothing more.¶

  -02: closed -- aat_hash binds the PoP JWT to the exact leaf instance (J.20.7), and through par_hash to the whole chain above it. A present aat_aud always applies (J.6.4). -02 Section 9.5 covers replay across enforcement points.¶

6.4. Coverage (B24, B25)

• B24 (Section 3.3): empty constraint map and absent arguments. A tool with an empty constraint map accepts any arguments, while a tool with even one constraint rejects an invocation that leaves out a constrained argument, even one under wildcard. -01 Section 3.3 states both, but the step from "no constraints" to "one constraint" changes the meaning of every other argument, which is easy to misread. This implementation follows the text.¶

  -02: closed -- {} is equivalent to {"*": {"constraint_type": "wildcard"}}, normalized at steps 4p and 6b (J.8.1, J.8.2, J.19.15, J.22.17).¶

• B25: no published test vectors; the 41 vectors are ours. -01 came with no test vectors. The 41 vectors in verifier/vectors/aat/ were written for this report from its own reading of -01. They show that the implementation matches that reading, not that the reading matches the author's.¶

  -02: closed -- 229 author vectors; 229 of 229 agree here.¶

6.5. Underdetermined in -02 (C1 to C10)

These are points where the -02 text, as read by this implementer, admits more than one conforming behaviour. None is a claim of a defect. Each ends with what this implementation does.¶

• C1 (-02 Section 3.5; steps 3a, 4a, 7a): duplicate members in the protected header. Steps 3b, 4b and 7b reject duplicate member names in claims, and the notes to -02 Section 8 give parser divergence ([RFC8259], Section 4) as the reason. The JOSE header is not covered. [RFC7515], Section 4 lets a parser either reject such a header or keep the last member. With {"typ":"aat-pop+jwt",...,"typ":"aat+jwt"}, explicit typing then depends on the parser. This implementation: rejects at steps 3a, 4a and 7a.¶

• C2 (-02 Sections 3.4, 4.3.1): JSON nesting needed for MAX_CONSTRAINT_DEPTH. A constraint tree of the depth -02 recommends (32) nests about 2 x 32 JSON levels inside the payload. J.8.15 (permit) is 68 levels deep and J.8.16 is 70. A verifier whose JSON parser has a common default nesting limit of 64 denies J.8.15 at step 3b. -02 says nothing about parser nesting limits or how they relate to MAX_CONSTRAINT_DEPTH. This implementation: the aat-02 parser allows max(64, 2 * MAX_CONSTRAINT_DEPTH + 32) levels.¶

• C3 (step 2c): "minimal JSON parsing". -02 does not say which jti is extracted when the payload repeats jti with different values, nor whether a payload that is not valid JSON fails at step 2c. J.23.4 uses equal values and so avoids the question. This implementation: a tolerant parse that takes the first occurrence; the duplicate is then rejected at step 3b or 4b.¶

• C4 (-02 Section 3.5; step 3a): typ comparison. The text says typ "equals" aat+jwt. [RFC7515], Section 4.1.9 makes typ values case-insensitive and allows the application/ prefix to be omitted, so application/aat+jwt names the same type. -02 does not say whether application/aat+jwt or AAT+JWT is to be accepted. This implementation: exact string comparison, so both are denied.¶

• C5 (-02 Section 7.2; step 7d): aat_aud type and semantics. Table 5 of -02 types aat_aud as a string, but gives it "the semantics of the JWT aud claim" ([RFC7519], Section 4.1.3), which allows an array. Whether an array aat_aud naming the enforcement point is accepted is not stated: -02 Section 3.2 has aat_aud identify an enforcement point "by exact string comparison", which leans towards a string, while step 6c explicitly allows aud to be an array. This implementation: anything other than a matching string is denied.¶

• C6 (steps 3b, 3k): "the trust anchor whose key verified the signature". When two anchors share one key under different issuers (rotation, aliasing), "the" anchor is ambiguous: the text can be read as any of them or as exactly one. This implementation: accepts when the issuer of any anchor whose key verifies the signature equals iss. The suite's anchors have distinct keys, so no vector decides it.¶

• C7 (-02 Section 3.2): magnitude of NumericDates and depths. Integer syntax is required, but admissibility (-02 Section 3.4) applies only to arguments and constraint values. An exp such as 9007199254740993 is well-formed; comparing it as a double or exactly gives the same verdict only because of the other bounds (lifetime, skew). Minor. This implementation: compares as a double.¶

• C8 (steps 3l, 4b2): what makes cnf.jwk invalid. "Encodes a public key" is followed only by examples of private members. The suite expects a denial at 3l or 4b2 for an RSA kty carrying Ed25519 members (J.21.21), an X25519 curve (J.24.10) and a 31-byte x (J.24.11); the description of J.24.10 itself allows the denial to come at step 7a instead. -02 does not refer to the member validation of [RFC7517] or [RFC8037]. This implementation: requires kty OKP, crv Ed25519, a 32-byte x and no private members (d, p, q, dp, dq, qi, oth, k).¶

• C9 (step 6b): args "as written" when the binding has already parsed them. The duplicate-member check is possible only on the invocation's JSON text. -02 Section 3.4 obliges a binding to preserve exact numbers but says nothing about duplicates. This implementation: accepts args as JSON text (checked) or as an already-parsed object (documented as unable to carry either fault).¶

• C10 (step 3k): the root's iss "is a URI". No grammar is referenced (for example, absolute-URI of [RFC3986]). This implementation: scheme ":" followed by non-space characters. Minor; no vector tests a borderline form.¶

9.1. aat

Organization:

None (individual).¶

Name:

aat (verifier and model).¶

Description:

A minimal TypeScript verifier for AAT-01, AAT-02 and asor-02 chains, and a ProVerif model of AAT-01 and asor-02; see Section 4 and Section 5.¶

Level of maturity:

Research prototype; an executable specification, not a product.¶

Coverage:

Chain verification only; no minting service, no CBOR, no revocation. asor-02: the token format (Section 3), authority and subsumption (Section 4), chain linkage (Section 5) and the offline verification algorithm (Section 6) through the action check (step 8), with DPoP holder binding (Section 7) for EdDSA proofs; not status lists (step 7, Section 8), mTLS confirmation or ES256 proofs. AAT-01: the root, link and leaf checks of Section 7 (invariants I1 to I6 of Section 4), the nine constraint types and their subsumption (Sections 3.4 and 4.5) and the PoP JWT (Section 5); not root issuance (Section 3.7) or derivation (Section 6) beyond test-only minting, keys other than Ed25519, or a PoP replay cache. AAT-02: every step of -02 Section 8, with the constraint map, well-formedness and subsumption rules of -02 Sections 3.3, 3.4 and 4.5 and the PoP JWT of -02 Section 7; not issuance or derivation (-02 Section 6), algorithms other than Ed25519, or extension constraint types (-02 Section 5).¶

Version compatibility:

draft-niyikiza-oauth-attenuating-agent-tokens-01, draft-niyikiza-oauth-attenuating-agent-tokens-02 and draft-asor-wimse-agent-delegation-chain-02.¶

Licensing:

Apache License 2.0.¶

Implementation experience:

The AAT-02 profile was written from the -02 text and then run against the author's vector suite; it agreed on all 229 vectors on the first run. Of the 25 observations made on AAT-01 while implementing it (Section 6), the -02 text decides 19 (16 closed, one of them by dropping the requirement, and 3 closed as design), decides one in part (B4), makes one moot (B8) and leaves four unchanged (B9, B12, B15, B18); ten points of the -02 text are underdetermined for an implementer (C1 to C10), and no vector decides any of them against this implementation. On asor-02 (Section 7) the main point is A1 with A7: Section 6 names no key for a link below the root, and the model states what the chain then guarantees; A2 to A6 are smaller gaps in the text and in the vectors' coverage. Where a draft was decidable the implementation followed it; where it was not, the choice is recorded in this document, not only in the code.¶

Contact:

Azat Davliatshin, ardavlyatshin@gmail.com¶

Information date:

2026-11-02¶

12.1. Normative References

[RFC2119]

Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, March 1997, <https://www.rfc-editor.org/rfc/rfc2119>.

[RFC7942]

Sheffer, Y. and A. Farrel, "Improving Awareness of Running Code: The Implementation Status Section", BCP 205, RFC 7942, DOI 10.17487/RFC7942, July 2016, <https://www.rfc-editor.org/rfc/rfc7942>.

[RFC8174]

Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, May 2017, <https://www.rfc-editor.org/rfc/rfc8174>.

12.2. Informative References

[AAT-01]

Niyikiza, N., "Attenuating Authorization Tokens for Agentic Delegation Chains", Work in Progress, Internet-Draft, draft-niyikiza-oauth-attenuating-agent-tokens-01, 2026, <https://datatracker.ietf.org/doc/draft-niyikiza-oauth-attenuating-agent-tokens/01/>.

[AAT-02]

Niyikiza, N., "Attenuating Authorization Tokens for Agentic Delegation Chains", Work in Progress, Internet-Draft, draft-niyikiza-oauth-attenuating-agent-tokens-02, 2026, <https://datatracker.ietf.org/doc/draft-niyikiza-oauth-attenuating-agent-tokens/02/>.

[AGNIHOTRI-02]

"Implementation Status of OAuth Identity Chaining and Transaction Tokens", Work in Progress, Internet-Draft, draft-agnihotri-oauth-agent-impl-status-02, 2026, <https://datatracker.ietf.org/doc/draft-agnihotri-oauth-agent-impl-status/02/>.

[ASOR-02]

Asor, R., "Verifiable Attenuated Delegation for AI Agent Chains", Work in Progress, Internet-Draft, draft-asor-wimse-agent-delegation-chain-02, 2026, <https://datatracker.ietf.org/doc/draft-asor-wimse-agent-delegation-chain/02/>.

[MADDEN-REVIEW]

Madden, N., "Review of draft-niyikiza-oauth-attenuating-agent-tokens-01 on the OAuth list", 2026, <https://mailarchive.ietf.org/arch/msg/oauth/9RkGndj2O23qOTvv1IRHlJjc0Cg/>.

[PROVERIF]

Blanchet, B., "ProVerif: Cryptographic protocol verifier in the formal model", n.d., <https://bblanche.gitlabpages.inria.fr/proverif/>.

[RFC3986]

Berners-Lee, T., Fielding, R., and L. Masinter, "Uniform Resource Identifier (URI): Generic Syntax", STD 66, RFC 3986, DOI 10.17487/RFC3986, January 2005, <https://www.rfc-editor.org/rfc/rfc3986>.

[RFC7515]

Jones, M., Bradley, J., and N. Sakimura, "JSON Web Signature (JWS)", RFC 7515, DOI 10.17487/RFC7515, May 2015, <https://www.rfc-editor.org/rfc/rfc7515>.

[RFC7517]

Jones, M., "JSON Web Key (JWK)", RFC 7517, DOI 10.17487/RFC7517, May 2015, <https://www.rfc-editor.org/rfc/rfc7517>.

[RFC7519]

Jones, M., Bradley, J., and N. Sakimura, "JSON Web Token (JWT)", RFC 7519, DOI 10.17487/RFC7519, May 2015, <https://www.rfc-editor.org/rfc/rfc7519>.

[RFC7638]

Jones, M. and N. Sakimura, "JSON Web Key (JWK) Thumbprint", RFC 7638, DOI 10.17487/RFC7638, September 2015, <https://www.rfc-editor.org/rfc/rfc7638>.

[RFC7800]

Jones, M., Bradley, J., and H. Tschofenig, "Proof-of-Possession Key Semantics for JSON Web Tokens (JWTs)", RFC 7800, DOI 10.17487/RFC7800, April 2016, <https://www.rfc-editor.org/rfc/rfc7800>.

[RFC8037]

Liusvaara, I., "CFRG Elliptic Curve Diffie-Hellman (ECDH) and Signatures in JSON Object Signing and Encryption (JOSE)", RFC 8037, DOI 10.17487/RFC8037, January 2017, <https://www.rfc-editor.org/rfc/rfc8037>.

[RFC8141]

Saint-Andre, P. and J. Klensin, "Uniform Resource Names (URNs)", RFC 8141, DOI 10.17487/RFC8141, April 2017, <https://www.rfc-editor.org/rfc/rfc8141>.

[RFC8259]

Bray, T., Ed., "The JavaScript Object Notation (JSON) Data Interchange Format", STD 90, RFC 8259, DOI 10.17487/RFC8259, December 2017, <https://www.rfc-editor.org/rfc/rfc8259>.

[RFC8785]

Rundgren, A., Jordan, B., and S. Erdtman, "JSON Canonicalization Scheme (JCS)", RFC 8785, DOI 10.17487/RFC8785, June 2020, <https://www.rfc-editor.org/rfc/rfc8785>.

[RFC9068]

Bertocci, V., "JSON Web Token (JWT) Profile for OAuth 2.0 Access Tokens", RFC 9068, DOI 10.17487/RFC9068, October 2021, <https://www.rfc-editor.org/rfc/rfc9068>.

[RFC9278]

Jones, M. and K. Yasuda, "JWK Thumbprint URI", RFC 9278, DOI 10.17487/RFC9278, August 2022, <https://www.rfc-editor.org/rfc/rfc9278>.

[RFC9396]

Lodderstedt, T., Richer, J., and B. Campbell, "OAuth 2.0 Rich Authorization Requests", RFC 9396, DOI 10.17487/RFC9396, May 2023, <https://www.rfc-editor.org/rfc/rfc9396>.

[RFC9449]

Fett, D., Campbell, B., Bradley, J., Lodderstedt, T., Jones, M., and D. Waite, "OAuth 2.0 Demonstrating Proof of Possession (DPoP)", RFC 9449, DOI 10.17487/RFC9449, September 2023, <https://www.rfc-editor.org/rfc/rfc9449>.

[RFC9864]

Jones, M.B. and O. Steele, "Fully-Specified Algorithms for JSON Object Signing and Encryption (JOSE) and CBOR Object Signing and Encryption (COSE)", RFC 9864, DOI 10.17487/RFC9864, October 2025, <https://www.rfc-editor.org/rfc/rfc9864>.

B.1. -00

Written against AAT-01 and asor-02; extended for AAT-02 after 26 October 2026 with the aat-02 verifier profile and the result of the author's vector suite.¶