Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .changeset/book-session-profiles.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
---

Book-only: specify session profiles and allocate the correct profile's extension type; nothing ships.
4 changes: 2 additions & 2 deletions book/src/api-reference.md
Original file line number Diff line number Diff line change
Expand Up @@ -237,8 +237,8 @@ PQ side-band (see [Session Lifecycle](./session-lifecycle.md)): `my_pq_turn`,
legs — `pq_ratchet_respond` / `pq_ratchet_bind` and `pq_rekey_respond` / `pq_rekey_apply`. **There
is no `pq_ratchet_begin` / `pq_rekey_begin`: the session self-drives A.4 and A.5.** On each
`encrypt`, when it is our turn and the side-band is idle, the session auto-stages the next round's
opening frame (A.5 on a credential lag — announcing the session's current principal as the handoff
— else A.4), and the host takes it from `pq_pending_outbound`/`pq_take_pending_outbound` to send
opening frame (A.5 on a credential lag — carrying the session's current principal onto our leaf
as the handoff — else A.4), and the host takes it from `pq_pending_outbound`/`pq_take_pending_outbound` to send
alongside the message. A.3 bootstrap stays host-driven (`pq_bootstrap_begin`, whose `rotating`
parameter carries the principal credential handoff and must name the session's current principal).
The A.4 ratchet and A.3 bootstrap have no separate `apply` call: the initiator ingests the
Expand Down
26 changes: 25 additions & 1 deletion book/src/group-rules.md
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,29 @@ reusable layer: an `MlsRules` filter every client is built with
(the first adopter binds `H(domain-tag ‖ role-ordered did:did)`); the crate never
interprets the bytes. Leaves advertise the extension type, so a binding-carrying
group can only ever contain capability-bearing leaves.
9. **The session profile is chosen from the two key packages and written once.** A
session runs one profile for its whole life (see
[Session Lifecycle](./session-lifecycle.md#session-profiles)). The default,
deployed-compatible, needs no signal. Every other profile has its own extension type,
which a classical key package's leaf lists in its capabilities when its client can
start a session in that profile: `CorrectProfile` (`0xF0A3`) for the correct profile.
A session runs a non-default profile only when both parties' classical key packages
advertise it, and runs the newest profile both advertise. Those are the classical half
of the acceptor's published combiner key package, which the initiator holds, and the
initiator's return key package, which the acceptor receives, so both parties compute
the same choice from signed key packages, with no negotiation message. The
chosen profile is recorded as a GroupContext extension of that profile's type, with
empty contents, written at creation into the classical half of the initiator's send
group and riding the Welcome. The default profile records nothing. A record with
contents, or more than one record, is rejected. The acceptor checks the recorded
profile against its own computation and mirrors it onto its return group, and the
initiator requires the return welcome to carry it back unchanged — all
`SessionProfileMismatch`, and on the invitation path raised before any invitation
state is claimed. PQ halves carry none (a PQ-half record is rejected at every PQ
join), and rule 1's GroupContextExtensions ban makes it immutable. As with the
AppBinding, leaves keep advertising the recorded type, so a profile-carrying group can
only ever contain capability-bearing leaves. The PQ key package's leaf need not list
it.

## Enforcement map

Expand All @@ -94,6 +117,7 @@ checks each cover ingress the others cannot see.
| Epoch discipline | — | staple-epoch compare in `process_incoming` (`EpochDesync` / skip) |
| Identity binding at establishment | — | `expected_remote` pre-claim check; creator-leaf ≡ key-package check at join; A.3 bootstrap KP hash-commitment check (`BootstrapKpMismatch`) |
| App-state binding at establishment | GCE ban keeps it immutable post-creation | `verify_app_binding` against `expected_app_binding` at `receive`/`accept` (post-join, pre-claim) and against the session's own binding at the initiator's return-welcome join; `verify_pq_half_unbound` at every PQ-half join (the binding lives on the classical halves only); empty bindings rejected at creation and as expectations (all `AppBindingMismatch`); leaf capability advertisement keeps uncapable leaves out of bound groups |
| Session profile at establishment | GCE ban keeps it immutable post-creation | not implemented in this crate: it advertises no profile, so a conforming peer never records one in a group it shares, and each session it runs is deployed-compatible |

Two properties worth naming:

Expand Down Expand Up @@ -168,5 +192,5 @@ rebindable view, and the sequences ride the session archive.

A refusal surfaces as `CredentialRejected` and is **retryable** where it arises from
a staple: the staple re-rides every frame, so approve-and-reprocess recovers the
round. `new_sender` / `new_recipient` are event hints; zxvbbvsv=`their_principal_state()` /
round. `new_sender` / `new_recipient` are event hints; `their_principal_state()` /
`my_principal_state()` are the truth.
4 changes: 3 additions & 1 deletion book/src/header-encryption.md
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,15 @@ a host may skip `open_incoming` for the message path. The initiator's initial we

## What leaks today

The table lists what the bare MLS fields expose; every frame travels sealed (under the header seal, or for the initiator's initial welcome inside the §A.1 HPKE envelope), so only the two parties see them, never a network observer.

| Field | Where | What an observer learns |
|---|---|---|
| frame tag (`0x01`–`0x1D`) | first byte of every tagged frame | frame kind: establishment vs. rotation vs. PQ side-band activity (bootstrap, ratchet, re-key) |
| `group_id` | every `MLSMessage` | a stable per-direction session identifier — links every message of a direction across epochs, undoing the per-epoch rendezvous rotation for anyone who stores ciphertexts |
| `epoch` | every `MLSMessage` | commit cadence, message ordering, session age |
| `content_type` | every PrivateMessage | application vs. proposal vs. commit |
| `authenticated_data` | every PrivateMessage | the 32-byte per-round proposal hash; on rotation frames and A.5 `Upd'` proposals, the announced `ClientId` |
| `authenticated_data` | every PrivateMessage | the 32-byte per-round proposal hash; on rotation frames, and on an id-changing A.5 `Upd'` in the deployed-compatible [session profile](./session-lifecycle.md#session-profiles), the announced `ClientId` |
| Welcome plaintext | APQWelcome (both halves) | cipher suites, `KeyPackageRef`s of the joiner — linkable to published key packages |
| MLS version / wire format | every `MLSMessage` | protocol fingerprint |

Expand Down
2 changes: 1 addition & 1 deletion book/src/protocol-flows.md
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ In its place we have two PQ operations:

One round re-keys ONE group; the turn alternation brings the other group’s round next. The large updatePath commit happens in isolation on the PQ group, otherwise we block the classical ratchet on transmitting it — only the small pathless ack rides the classical staple.

**Who opens a round — the session, not the host.** The host never selects or opens A.4/A.5; the session self-drives them. Whenever it is our turn, the PQ side-band is idle and not wedged, and both halves are live (post-A.3), the next `encrypt` opens the next round automatically: an **A.5 re-key** if either leaf in the PQ half of our receive group (the group our A.5 re-keys) lags, else an **A.4 ratchet**. A leaf *lags* when it presents a credential id other than its owner's *current* canonical (classically committed) id; a same-id key refresh is not a lag. If the lagging leaf is ours, the round is the credential catch-up: our `Upd'` announces our identity. If it is the peer's, the round is the reciprocal catch-up: the peer's responder `Commit'` carries theirs. Opening is send-driven and best-effort (a transient staging failure just retries on the next send), and the frame it stages rides that same send's re-staple. So the abstract "initiator (Alice) sends…" above is, concretely, *Alice's next ordinary message once the turn is hers*. One subtlety: a rotation that lands while an A.4 is staged, or while an A.5 `Upd'` is in flight, does not re-mint that round, and a responder whose own rotation staple has not yet applied answers with a `Commit'` that moves nothing. Either way the leaf still lags after the round and the next turn's trigger opens the catch-up — a race costs one extra round, never a stall. The deployed Rust engine deviates here after a one-sided rotation; see [Shipped anomalies](./session-lifecycle.md#shipped-anomalies).
**Who opens a round — the session, not the host.** The host never selects or opens A.4/A.5; the session self-drives them. Whenever it is our turn, the PQ side-band is idle and not wedged, and both halves are live (post-A.3), the next `encrypt` opens the next round automatically: an **A.5 re-key** if either leaf in the PQ half of our receive group (the group our A.5 re-keys) lags, else an **A.4 ratchet**. A leaf *lags* when it presents a credential id other than its owner's *current* canonical (classically committed) id; a same-id key refresh is not a lag. If the lagging leaf is ours, the round is the credential catch-up: our `Upd'`'s new leaf carries our current identity. We open it only once the peer has folded the classical offer that moved our leaf to our current id, so our leaf in the classical half of the peer's send group already presents it; until then the turn opens an A.4, because the peer admits a move only to an id it has committed. If it is the peer's, the round is the reciprocal catch-up: the peer's responder `Commit'` carries theirs. Opening is send-driven and best-effort (a transient staging failure just retries on the next send), and the frame it stages rides that same send's re-staple. So the abstract "initiator (Alice) sends…" above is, concretely, *Alice's next ordinary message once the turn is hers*. One subtlety: a rotation that lands while an A.4 is staged, or while an A.5 `Upd'` is in flight, does not re-mint that round, and a responder whose own rotation staple has not yet applied answers with a `Commit'` that moves nothing. Either way the leaf still lags after the round and the next turn's trigger opens the catch-up — a race costs one extra round, never a stall. The deployed Rust engine deviates here after a one-sided rotation; see [Shipped anomalies](./session-lifecycle.md#shipped-anomalies).

1. Session establishment
1. Bob posts an APQ keyPackage
Expand Down
43 changes: 36 additions & 7 deletions book/src/session-lifecycle.md
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,8 @@ frame rides that send's re-staple peek (`pq_pending_outbound`), so the host's ro
send groups' PQ halves **alone**, so the classical ratchet is never blocked behind a large
ML-KEM updatePath. It is not a host call either: the session opens it in place of an A.4 when
either leaf in the PQ half of our receive group lags its owner's canonical principal. When
that leaf is ours (a Phase 8 classical rotation moved the session client), our `Upd'`
announces our principal as the handoff. When it is the peer's, the peer's responder `Commit'`
that leaf is ours (a Phase 8 classical rotation moved the session client), our `Upd'`'s
new leaf carries our principal as the handoff. When it is the peer's, the peer's responder `Commit'`
carries the peer's principal onto its own send-PQ leaf: the reciprocal catch-up. The
initiator's send auto-stages `Upd'(self)` into the PQ half of the peer's send group (`0x1B`);
the responder commits it with its own `Commit'` (`pq_rekey_respond`, `0x1D`) — whose updatePath
Expand Down Expand Up @@ -202,8 +202,8 @@ moves at its next approved commit (the peer observes `new_sender` on that staple
message attribution follows). A PQ leaf minted at A.3 is born under its owner's
then-canonical id; every other PQ leaf catches up over A.5 rounds, one per PQ group, which
the session self-drives. The rotated party's own
A.5 announces its *current*, already-canonical principal in the PQ half of the peer's
send group, and the handoff's new leaf carries that credential. The peer's next turn then
A.5 carries its *current*, already-canonical principal onto its leaf in the PQ half of
the peer's send group. The peer's next turn then
opens the reciprocal A.5, because the rotated party's leaf in the peer's receive group
still lags. The rotated party answers as responder, and its `Commit'` carries the
credential onto its own send-PQ leaf. The acceptor's recv-group leaf
Expand Down Expand Up @@ -254,6 +254,35 @@ to this crate — the caller picks the convention (Germ's adapter digests the en
STABLE PREFIX — the app payload, else the bare welcome — so every pre-establishment
re-staple from the same initiator resolves to the same token).

## Session profiles

The behavior this book specifies is the *correct* profile. A second profile,
*deployed-compatible*, adds two behaviors that keep a session with the deployed engine
healthy:

- **Announced id.** An A.5 `Upd'` that changes its leaf's credential id also carries the
new id in its authenticated data. A key-only `Upd'` carries none. Deployed hosts read
the announced id to trigger reconciliation.
- **Deferred reciprocal.** The reciprocal A.5 waits until the peer's own A.5 has landed,
meaning the peer's leaf in our send-PQ group presents its current canonical id. Until
then our turn opens an A.4, so the peer can still run its own round. This is the
accommodation for anomaly 5 below. The correct profile opens the reciprocal as soon as
the peer's leaf lags.

In both profiles a receiver accepts an `Upd'` whose authenticated data is empty or equals
the new leaf's credential id, and rejects any other value.

Deployed-compatible is the default and is frozen: it changes only to fix a defect or to
follow the deployed engine. The profile is chosen once per session, from the two key
packages ([Group Rules](./group-rules.md), rule 9), and never changes, not even when a peer
upgrades. A client advertises a profile only once it implements that profile completely.
The deployed engine advertises none, so every session with it runs deployed-compatible,
and so does every session created before profiles existed. A session migrated from the
deployed engine is deployed-compatible too; its groups carry no record. Two clients that both
advertise the correct profile start in it, with no flag day. A later wire-visible change
to the correct behavior ships as a new profile with its own extension type, never as a
change to a shipped one.

## Shipped anomalies

This book specifies intended behavior. The deployed Rust engine, and the card host it
Expand Down Expand Up @@ -295,9 +324,9 @@ engine, or needing an accommodation beyond the spec.
rejected, and the presented key survives only as its own send-PQ group's signer.
When it later answers a peer's A.5, its responder `Commit'` replaces that signer,
and the leaf is orphaned for good: no copy of its key remains.
- *Resolution: needs an accommodation.* A conforming peer defers a reciprocal A.5
until the peer's own A.5 has succeeded, meaning the peer's leaf in our send-PQ
group is current. Against a conforming peer this costs at most one extra round.
- *Resolution: needs an accommodation:* the deployed-compatible profile's deferred
reciprocal ([Session profiles](#session-profiles)), which every session with the
deployed engine runs. Against a conforming peer it costs at most one extra round.
A conforming engine that takes the party over drops its mis-signed parked `Upd'`
and re-proposes under the carried key, which heals it. Once the leaf is orphaned,
nothing heals it.
Expand Down
17 changes: 17 additions & 0 deletions book/src/wire-format.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,13 @@ HPKE plaintext (see "The §A.1 envelope" below).
| `PQ_REKEY_UPD_TAG` | `0x1B` | PQ re-key: initiator's `Upd'` proposal |
| `PQ_REKEY_COMMIT_TAG` | `0x1D` | PQ re-key: the responder's `Commit'` |

Every MLS object a TwoMLSPQ frame carries is a complete RFC 9420 `MLSMessage`, never a
bare struct: each `APQWelcome` half, every key package (the published halves, the §A.1
return key package, and the `0x13` KP′), every commit and proposal (including the A.5
`Upd'` and `Commit'`), and every PrivateMessage (including the `0x09` app staple and the
`0x17`/`0x19` legs). The envelope describes its own protocol version and content type, so
a receiver never infers either from the frame tag alone.

There is no bind tag: a round's closing bind is the **message-frame staple** (the
`APQPrivateMessage` above), not a side-band frame, so every side-band frame is answered by
its round's next leg.
Expand Down Expand Up @@ -315,6 +322,16 @@ Every occupied leaf must advertise the `APQInfo` extension (`0xF0A1`) and the
`AppDataUpdate` proposal (`0x0008`) types; a leaf that cannot support them is rejected
rather than silently degraded.

The extension and proposal types these frames use. The extension types sit in RFC 9420's
private-use range (`0xF000`–`0xFFFF`):

| Type | Value | Kind | Specified in |
|------|-------|------|--------------|
| `AppDataUpdate` | `0x0008` | proposal | [group rules](./group-rules.md), rule 7 |
| `APQInfo` | `0xF0A1` | GroupContext extension | [group rules](./group-rules.md), rule 7 |
| `AppBinding` | `0xF0A2` | GroupContext extension | [group rules](./group-rules.md), rule 8 |
| `CorrectProfile` | `0xF0A3` | GroupContext extension; leaf capability entry | [group rules](./group-rules.md), rule 9 |

## Invariants

The tag values are part of the on-wire protocol; pre-release, a renumber is allowed. When
Expand Down
Loading