Packages
Deterministic protocol verification for cryptographically bounded proof-of-possession authority.
Current section
Files
Jump to
Current section
Files
docs/guides/implementers-guide.md
# The implementer's guide: building a conforming BAP verifier
Everything a fifth implementer needs to build a verifier that passes the conformance corpora —
without reading any sibling runner's source. Start with contract-major 1: its specification
(`spec/bap-v1.md` in the repository; the package ships it) is the normative authority, and
contract-majors 2 and 3 incorporate it by reference (§14). This guide is the operational recipe.
## 1. Read in this order
1. The specification — sections 4 (conformance language), 7 (abstract data model), 8-9
(JSON decoding, base64url), 10-14 (protected headers, claims, selectors, URI normalization,
signing and digest inputs, including 14.1 strict Ed25519), 15 (consumption chain and anchored
export), 16 (public verification contract), 17 (hard maxima), and 18 (untrusted key
locator).
2. The requirement map (`docs/design/requirement-map.md`) — every `REQ1-*` id to its
conformance evidence cells.
3. This guide, then the corpus.
## 2. The conformance-runner contract
A conforming runner:
1. Loads the corpus directory: `index.json` (the integrity binding), the per-file case JSON,
any `.raw` sidecars, and the `revision.json` sidecar (see §5).
2. Asserts the corpus identity at startup: the base64url SHA-256 of `index.json`'s exact bytes
against the certified digest recorded in your runner (rotate it only in the same change as
the corpus — the repository ships a regeneration script).
3. Verifies corpus integrity itself: per-file SHA-256 against the index, exact file-set
equality both directions, per-file and total case counts, corpus-wide case-id uniqueness,
the applicability matrix (every surface × class cell: declared count equals executed
count; `n_a` cells execute zero), and every tamper case's verbatim artifact re-derived
from its base case with the documented single-byte xor flip.
4. Executes every case: dispatch by `surface`, apply the case's `input`, compare the outcome
to `expected.verdict` — valid cases must produce the expected value-bearing facts;
invalid cases must produce the single closed error value, with no other observable.
5. Prints a machine-readable agreement report and exits nonzero on any disagreement.
Verdict comparison is total: a crash, exception, timeout, or "unsure" on ANY case is a
failure, not a skip. The reference implementations abort the run on any non-protocol error
distinct from a clean rejection.
## 3. The dispatch table
Dispatch is keyed on the case's `surface` field. The 28 surfaces:
| Surface | What it exercises |
|---|---|
| `untrusted_key_locator` | Header-only grant inspection; payload stays opaque |
| `grant_signing_input` / `proof_signing_input` | Deterministic producer: exact JWS signing input |
| `encode_consumption_entry` | Producer: canonical consumption row bytes |
| `check_chain` | Hash-chain verification over raw row bytes and caller boundaries |
| `boundary_anchor_signing_input` / `key_transition_signing_input` | Producers for anchor/transition JWS inputs |
| `encode_anchored_export` | Producer: framed archive bytes |
| `assemble_compact` | Compact JWS assembly from a signing input and a signature |
| `decode_grant` / `decode_proof` | Bounded closed decode (no signature check) |
| `verify_grant` | Grant verification against a trusted issuer and expected context |
| `verify_historical_anchor` / `verify_key_transition` | Historical-key path authentication |
| `verify_anchored_export` | Complete-archive verification (chunks, version, boundaries) |
| `check_envelope` | Combined grant+proof request verification |
| `request_digest` | The domain-separated digest over `[operation, typed(cast_arguments)]` |
| `jcs.encode` | RFC 8785 canonical serialization from the tagged algebra |
| `jwk.encode_public` / `jwk.decode_public` | Closed public OKP JWK handling |
| `jwk.thumbprint_preimage` / `jwk.thumbprint` / `jwk.thumbprint_raw` / `jwk.public_key_thumbprint_raw` | RFC 7638 thumbprints |
| `uri.normalize` | HTTPS URI normalization |
| `json.decode` | The bounded ordered JSON decoder |
| `base64url.decode` | Strict base64url |
| `bounds.new` | Tightening-only bounds construction |
The live authority for this enumeration is the corpus index's `applicability` key set; the
repository's drift gate cross-checks this guide's table against it (see §7).
## 4. The two-boundary key census
The corpus pins its public-key set two ways: every case's key-bearing inputs are fingerprinted
at DISCOVERY (the runner records every public key it encounters while executing) and at
VERIFY-IMPORT (the runner records every key actually passed to its cryptographic verify
primitive). A conforming run asserts:
```
discovered == verify-imported == index.public_key_fingerprints
```
two-way equal. This catches the two classic runner cheats: never actually verifying (empty
verify-import), and accepting fabricated keys (verify-import ⊄ corpus set). The reference
run reports 11 keys.
## 5. Corpus formats
- `index.json` — closed 5-member object: `format`, `public_key_fingerprints`, `files`
(path, per-file base64url SHA-256, per-file case count), `total_cases`, `applicability`.
- `revision.json` — the corpus revision sidecar: closed 3-member object (format, monotone
integer `revision`, `generated_from` provenance), hash-covered as a `files` entry and
enforced by file-set equality. Citation target for corpus-dependent documents.
- Case files — closed objects (`format`, `provenance`, `cases`); every case carries `id`,
`surface`, `class`, `input`, `expected`. Structural schemas (Draft 2020-12) ship under
`priv/conformance/v1/schemas/`.
- `.raw` sidecars — opaque byte inputs, hash-bound, never parsed.
## 6. The permissiveness-mutation expectation
Your implementation must not be MORE permissive than the reference. The corpus catches most
of this by disagreement, but each language has its own trap class — prove each of these
red-capable in YOUR language (construct the defect, assert your runner rejects it, then
mechanically remove the guard and watch the test go green — that survivor is the bug):
- **Duplicate-member rejection at every depth** (e.g. `{"a":1,"a":1}`) — most language JSON
parsers silently keep the last member.
- **Null-prototype equivalence** (the JS `__proto__` class) — constructing objects with
prototype inheritance can make two distinct values canonicalize identically; use
prototype-free dictionaries for the tagged algebra.
- **Raw numeric-lexeme ceiling** — the 64-byte ceiling applies to the RAW lexeme before
conversion, with exact decimal magnitude comparison (no floating-point rounding).
- **Single-value, no trailing content** — input is exactly one complete JSON value plus
whitespace.
- **Integer/float tag distinction** — `1` and `1.0` are different typed values with different
request-digest projections; a language that unifies them cannot produce conforming digests.
- **Decode-depth scalar asymmetry** — containers are depth-bounded, scalars are not: a
maximum-depth-inner SCALAR is valid where a maximum-depth-inner container is not.
## 7. Embedding the spec: the facts-anchor contract
If you embed or derive tooling from the specification: its normative tables carry
`<!-- facts:key -->` anchors (ten closed keys); a byte-deterministic extraction of the
anchored regions is the drift contract between spec, implementation, corpus, and requirement
map. The repository's own gates (extraction equality against a frozen baseline; closed-set
containment of corpus unions; requirement-map reconciliation; keyword census; anchor
completeness) are the reference implementation of that contract.
## 8. Proving it
Run the corpus. A conforming implementation reports 283/283 agreement, census two-way
equality, and the certified index digest. The reference CLI ships in the package as the shape
of the expected output. When you publish, the repository's interoperability record is where
independent implementations record their results.
## 9. Implementing the local-loopback application profile
The standard corpus above remains unchanged. The byte-distinct local-development profile is a
sibling contract defined by `spec/bap-local-loopback-http-v1.md` and certified independently under
`priv/conformance/application-profiles/local-loopback-http/v1`.
A conforming implementation exposes five separately named surfaces: URI normalization, proof
signing-input production, compact assembly, proof decode, and envelope verification. It admits
only literal `127.0.0.1` and `[::1]` HTTP authorities, requires a nonce, signs protected
`typ: "ba+loopback-proof"`, and never infers or retries the standard profile. Pin the exact profile
index SHA-256 (`10fc4cf05affcddc9e6340ff392c247e25ab038cd938f2557829a7ce63b1a5e4`), verify the declared
two-file set and per-file hashes, execute all 36 URI and 8 proof cases, then prove both directions
of cross-profile rejection. The repository's real-socket drill additionally exercises IPv4 and
IPv6 listeners plus a verifier-bypass mutation; self-round-trip corpus agreement alone is not
transport evidence.
## 10. Implementing the role-attestation sibling profile
The standard corpora remain unchanged. The role attestation is the protocol's first sibling
attestation profile: a standalone, grant-unbound compact defined by
`spec/bap-role-attestation-v1.md` and certified under
`priv/conformance/attestation-profiles/role-attestation/v1`.
A conforming implementation exposes four separately named surfaces: attestation signing-input
production, compact assembly, attestation decode, and attestation verification. The protected
header is exactly `{alg: "EdDSA", kid, typ: "ba+role-attestation"}`; the payload is exactly
`{v: 1, jti, key_id, public_key, role, nbf, exp}` with `role ∈ {"issuer", "holder"}` and
canonical JCS bytes. Verification takes the caller-supplied attestor key (with its own validity
window), the expected subject binding, and `now`; it enforces the attestor-kid binding, the
subject binding, structural self-attestation rejection, window containment (the attestation
window inside the attestor key window), and the half-open `[nbf, exp)` now-window, returning
redacted facts with `trust: :not_evaluated` and no authorization marker. Pin the exact profile
index SHA-256 (`be5275c69539a0f31734242ff00a484c2f855f39181c55689d8b0f671195d62a`), verify the
declared two-file set and per-file hashes, execute all 40 cases, and prove cross-profile
rejection in both directions. Derive every fingerprint with the RFC 7638 Ed25519 thumbprint
preimage — never a hash of raw key bytes.
## 11. Implementing the content-assertion sibling profile
The content assertion is the second sibling attestation profile: a standalone,
grant-unbound compact defined by `spec/bap-content-assertion-v1.md` and certified under
`priv/conformance/attestation-profiles/content-assertion/v1`.
The protected header is exactly `{alg: "EdDSA", kid, typ: "ba+content-assertion"}`. The payload
is exactly the thirteen members `v`, `jti`, `iss`, `aud`, `sub`, `profile`, `profile_digest`,
`content_digest`, `gen`, `prev`, `iat`, `nbf`, and `exp`, in canonical JCS bytes. The three
digests are canonical unpadded base64url of exactly 32 bytes; `gen == 1` exactly when `prev` is
32 zero bytes; structural time is `iat <= nbf < exp`.
`content_digest` is SHA-256 over `UTF8("BAP1-CONTENT") || 0x00 || content`, for 1 through
`content_bytes` (65,536) bytes, and never parses the content. `assertion_digest` validates the
compact as this profile and hashes its exact bytes with unprefixed SHA-256; it is the value a
successor names in `prev`. Verification takes one caller-selected attestor key and window, the
expected issuer, audience, subject, profile, profile digest, content digest, and `now`. It checks
the kid binding, every expected value, key-window containment (`exp` may equal a finite
`valid_before`), the half-open `[nbf, exp)` window, and the Ed25519 signature, returning redacted
facts with `trust: :not_evaluated` and no authorization marker. Pairwise successor verification
accepts only complete facts values and requires equal context, `gen + 1`, `prev` equal to the
predecessor's digest, nondecreasing `iat`, and a different `jti`.
Pin the exact profile index SHA-256
(`14b7436ccf7cc91fece52a1578c3760df6720a93494d147ee5ab523e2ce21876`), verify the declared
eight-file set and per-file hashes, execute all 131 assertion, 9 digest, and 14 successor cases,
compare producer and assembly bytes where the corpus supplies them, and prove cross-profile
rejection in both directions.
## 12. Implementing strict Ed25519 verification
Every Ed25519 surface uses one rule, specified in
[`spec/bap-v1.md` § 14.1](../../spec/bap-v1.md#strict-ed25519) and introduced by erratum 2 in
the [errata registry](../errata.md). Put it at your single Ed25519
verification point, ahead of the backend call:
1. Reject a non-canonical `A` or `R`: the low 255 bits read as `y >= p`, or one of the two
encodings that set the sign bit for a point with `x = 0`. This is a byte comparison, identical
in every language.
2. Reject `A` or `R` equal to any of the eight small-order encodings. Keep one table for both
checks, and derive the expected set in your tests by arithmetic (the multiples of a point of
order 8) instead of copying it.
3. Reject `S >= L`.
4. Verify with the cofactorless equation. Many backends compute it; a cofactored verifier (one
that multiplies by 8, as ZIP 215 style verifiers do) is non-conforming.
Key acceptance adds an on-curve check (the RFC 8032 §5.1.3 decoding succeeds) and applies to every
key that enters a verification input or a producer, including JWK decode, encode, and thumbprint
functions. Keep a separate hash-only thumbprint path for censuses and generators, and never use
it on a verification path. Expose a torsion-free check (`[L]A = O`) for hosts; never run it on the
verification path, since mixed-order keys verify by design.
Run the strict-Ed25519 corpus (`priv/conformance/strict-ed25519`, `bap-strict-ed25519/1`) beside
the existing corpora and pin its index SHA-256
`732117dfe1881b553998126a9524a95bfb1171257e388d5430a0a099f2287cb9` at load. Each case names its
surface, the requirement it isolates (`rule`), and, for signed artifacts, the major it targets.
The `primitive`, `key-acceptance`, and `differential` families exercise the rule directly; the
other families carry the same inputs through every signed surface. The rule-S1 checks for
canonical `R` and `S < L` are often duplicated by backends, so prove them with unit tests and
permissiveness mutants, not only with corpus verdicts.
## 13. Producer surfaces: assembly and export encoding
Compact assembly and anchored-export encoding are producer surfaces, governed by erratum 3 in
the [errata registry](../errata.md). The Elixir implementation and the corpus below are part of
release 0.9.0. These surfaces hold no key and verify no
signature, but they refuse a signature that no conforming signer emits and they never rewrite
the bytes they accept:
- Under contract-major 3, refuse any framed signature outside `0 < r < n`, `0 < s <= floor(n/2)`
with the closed error. Call the same predicate your verifier runs; do not keep a second copy of
`n` or `floor(n/2)`.
- Under Ed25519 (contract-majors 1 and 2 and the three sibling profiles), refuse a signature whose
`R` is non-canonical or of small order, or whose `S >= L`. This is the keyless part of rule S1:
factor it out of your verification gate so one function owns it, and do not decode `R` at
assembly.
- Never normalize at these surfaces. Normalization (`s <- n - s` when high) is the signer's duty:
the party that receives the signature from an HSM or KMS converts DER to the raw form and
normalizes before assembly. In Elixir, `BoundedAuthorityProtocol.Es256.der_to_raw/1` and
`normalize_low_s/1` do exactly that, and `BoundedAuthorityProtocol.Es256.canonical_signature?/1`
is the shared predicate.
- Decode stays untouched: a decoded compact is not a verified one.
Run the producer-canonicality corpus (`priv/conformance/producer-canonicality`,
`bap-producer-canonicality/1`) beside the existing corpora and pin its index SHA-256
`99ee6fbbf32758b03d4630647f721d8d4e349f0628d860493d667fe6e762c601` at load. Its 15 accepted
cases sit exactly at the rule's bound and must emit the signing input plus the signature
unchanged; their signatures are not verifiable. Add a permissiveness mutant that deletes your
assembly check and watch the 60 refused cases go red.
## 14. Contract-majors 2 and 3, and the selector float-zero rule
Contract-major 2 ([`spec/bap-v2.md`](../../spec/bap-v2.md), suite `BAP2-Ed25519-SHA256`) and
contract-major 3 ([`spec/bap-v3.md`](../../spec/bap-v3.md), suite `BAP3-ES256-SHA256`) are
complete closed profiles that incorporate contract-major 1 by reference with the substitutions
each specification lists in its § 2. Contract-major 2 adds the inclusive range selector kinds
`lte` and `gte`; contract-major 3 keeps that selector algebra and changes the signature suite to
ECDSA P-256 with raw `r || s` signatures and low-S canonicality. Each major parses only its own
bytes: dispatch on the payload `v` claim and never retry another major after a failure.
Run each major's certified corpus (`priv/conformance/v2/corpus`, 268 cases, and
`priv/conformance/v3/corpus`, 292 cases) with the same runner contract as §2, pinning each index
SHA-256 at load.
Erratum 6 adds one rule to the selector algebra of every major. Grant decode rejects an `equals`
value or `one_of` member that contains a float-tagged number equal to zero at any depth, whatever
its sign or spelling (`0.0`, `-0.0`, `-0e0`, an underflowing `1e-400`); range bounds and inert
`all` members are unchanged. The grant producer refuses any float-tagged integral selector value,
because its canonical bytes would decode integer-tagged. Test the decoded value, not the lexeme,
so underflow is covered. Run the additive selector float-zero corpus
(`priv/conformance/selector-float-zero`, `bap-selector-float-zero/1`, 161 cases) and pin its index
SHA-256 `97fd7a99cdbf3acc0a78f5ba1c6556e23a63e0ad66f533e31fd69f82dc5f3003` at load.