From 5c63baaa23479efb5d2d6f1824d1f9eb2b05f98e Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 00:55:46 -0800 Subject: [PATCH 1/6] chore(quest): claim quest/m1/route-key-model.md Quest-Claim: a5c946d1802b02ee From c67b784afeb268c5f01b3e7b0dbd7ff37f8b7ba6 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 01:03:31 -0800 Subject: [PATCH 2/6] test(net): a Tamarin model proves a route key proof binds to its session and side Co-Authored-By: Claude Opus 5.5 --- .claude/skills/verify-route-key/SKILL.md | 59 ++++++ .github/workflows/nightly.yml | 3 +- drafts/draft-lcurley-moq-lite.md | 7 +- quest/m1/route-key-model.md | 55 ------ quest/m2/lite07-finalize.md | 1 - rs/justfile | 5 + rs/moq-net/verify/route-key/RouteKey.spthy | 206 +++++++++++++++++++++ test/justfile | 4 + test/route-key-model.sh | 46 +++++ 9 files changed, 327 insertions(+), 59 deletions(-) create mode 100644 .claude/skills/verify-route-key/SKILL.md delete mode 100644 quest/m1/route-key-model.md create mode 100644 rs/moq-net/verify/route-key/RouteKey.spthy create mode 100755 test/route-key-model.sh diff --git a/.claude/skills/verify-route-key/SKILL.md b/.claude/skills/verify-route-key/SKILL.md new file mode 100644 index 0000000000..fe3b84a966 --- /dev/null +++ b/.claude/skills/verify-route-key/SKILL.md @@ -0,0 +1,59 @@ +--- +name: verify-route-key +description: Prove lite-07's Route Key Parameter (`rs/moq-net/src/route/proof.rs`, `js/net/src/lite/route_key.ts`) binds a key to its session and side with Tamarin. Use when a change touches what a route key proof signs or how it is checked, a transport binding's `export_keying_material`, TLS early data or resumption, or the draft's Route Key Parameter, or when a replay, reflection, or relaying attack on the proof needs every attacker strategy checked rather than a unit test. +--- + +# Verify the route key proof + +`rs/moq-net/verify/route-key/RouteKey.spthy` models the Route Key Parameter in Tamarin: each endpoint signs the domain, its side, and the session's exported secret, and its peer checks that signature against its own export. The attacker owns the network, makes keys of its own, and runs sessions with every endpoint, including as an intermediary that terminates TLS. Connections are TLS 1.3 full handshakes or resumptions, carrying one raw QUIC session (binding 1) or WebTransport sessions under attacker-chosen IDs (binding 2). Every run records which endpoint is really at its other end, so the lemmas judge a proof against the truth rather than an endpoint's belief. + +## Lemmas + +Every lemma must verify; the harm says why it matters. + +| Lemma | Holds when | Harm if broken | +| --- | --- | --- | +| `executable`, `executable_resumed_webtransport` | Two endpoints can accept each other's keys over raw QUIC, and over WebTransport after resumption. | The other lemmas hold vacuously. | +| `no_relay` | An honest key is never accepted on a session the attacker terminates. | An attacker, or a TLS-terminating intermediary, is filed under an honest relay's key and takes over its routes. | +| `no_reflection` | An endpoint accepts its own key only from itself, as the other side. | The attacker hands a relay its own proof and is filed as that relay. | +| `no_replay` | One signature is accepted on one session only. | A recorded proof claims a key on another connection. | +| `injective_agreement` | An accepted honest key was signed by the session's other end, for that side of that session, and no other session accepts it. | Any of the above. | + +## Variants + +Each variant drops one assumption the draft states and must break exactly the lemmas its `Breaks:` line names, which keeps the model from passing vacuously. + +| Variant | Drops | Breaks | +| --- | --- | --- | +| `NO_SIDE` | The side byte in the signed message. | `no_relay`, `no_reflection`, `injective_agreement` | +| `EARLY` | The main exporter: a resumed client signs over its 0-RTT secret, which a replayed ClientHello reproduces. | `no_replay`, `injective_agreement` | +| `NO_EMS` | A per-session secret: a man in the middle gives its two sessions one, as TLS 1.2 without RFC 7627 allows. | `no_relay`, `no_reflection`, `injective_agreement` | + +## Run + +```sh +just test route-key-model +just rs tamarin moq-net/verify/route-key/RouteKey.spthy -D=NO_SIDE +``` + +The first proves the model and checks every variant's `Breaks:` line, in about ten seconds; Nightly runs it. The second proves one variant. To read a counterexample, run `nix shell --inputs-from . nixpkgs#tamarin-prover --command tamarin-prover interactive rs/moq-net/verify/route-key/` and open the falsified lemma. + +## Reading a failure + +A falsified lemma is an attack path, not yet a bug. Check that each rule it fires matches the code: the transport bindings below for the secret, `proof.rs` for the message. If the code cannot take a step, fix the model. If it can, the signed transcript is wrong: fix it in Rust, JS, and the draft together, and keep `a_proof_matches_the_js_transcript` (Rust) and `route_key.test.ts` (JS) agreeing. Do not add a restriction or drop an attacker rule until a lemma verifies. + +## Coverage + +Sync commit: `23898b48f46cb54da19007279504b2b6ecdf80cf`. Run `git log 23898b48f4.. -- rs/moq-net/src/route/proof.rs js/net/src/lite/route_key.ts` and the files below to see what changed since. After a change to a covered function, mirror it in the model, rerun `just test route-key-model`, and move the sync commit forward only once the model describes the code at the new commit. + +| Code | Model | +| --- | --- | +| `rs/moq-net/src/route/proof.rs` `Transcript::message`, `Transcript::prove`, `DOMAIN`, `EXPORTER_LABEL` (and `sign` in `js/net/src/lite/route_key.ts`) | `Prove` | +| `rs/moq-net/src/route/proof.rs` `Transcript::verify` `rs/moq-net/src/lite/setup.rs` `PeerSetupState::set` | `Accept_from_server`, `Accept_from_client` | +| `rs/moq-net/src/lite/session.rs` `start` (and `proveRouteKey` in `js/net/src/lite/route_key.ts`) | `Session_quic`, `Session_webtransport`, `Prove` | +| `rs/moq-tokio/src/quic/web/session.rs` `webtransport_exporter_context` `rs/moq-uring/src/quic/web.rs` `webtransport_exporter_context` | `Session_webtransport` | +| `rs/moq-quic/src/crypto/rustls.rs` `QuicClientConfig::new`, `QuicServerConfig::new` (TLS 1.3 only, early data off) | `Connect`, `Resume`, and the `EARLY` and `NO_EMS` variants | + +## Not covered + +Ed25519 is an ideal signature: a small-order public key that verifies anything is a key no honest endpoint holds, which the attacker could share between its own sessions anyway. TLS is reduced to its exporter: a connection's two ends share a fresh secret, resumption mixes the PSK with fresh randoms, and server authentication plays no part, since the proof must hold even when the client dials the attacker. Out of scope: a compromised route key, and relays sharing one key on purpose, which the draft allows. Bindings 3 to 5 (qmux) export nothing, so they never send or rely on a proof. The memory transport and Firefox's WebTransport exporter, which `route_key.ts` skips for deriving the session ID differently, are not modelled. diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index d8ed5cbd0c..d12e1fa177 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -340,6 +340,7 @@ jobs: # `rs quic-sim` sweeps moq-quic's simulated workloads from a fresh seed; PRs run a fixed 64. # `rs rung-disable` proves FFI simulcast disable and recovery on a shaped BBR3 uplink. # `test resume-model` sweeps resume against its model from a fresh seed; PRs run a fixed 64. + # `test route-key-model` proves the route key proof with Tamarin, and that each variant breaks what it names. # It also runs the bandwidth probe's acceptance suite, of which PRs run the short cases. # `test drill impaired` runs the relay drills over a freshly seeded shaper; PRs run loopback. # `rs cli-export` runs moq-cli's export process tests, which take tens of seconds of real time. @@ -355,7 +356,7 @@ jobs: # `rs v4l2` streams moq-video's V4L2 capture from the kernel's vivid # virtual camera, a module load no pull request job should make. # `js worklet-matrix` loads `?worklet` output through the bundlers pinned in test/worklet. - recipe: ["gate", "gh test-integration", "rs doctest --workspace", "rs send-depth", "test drill-sensitivity", "rs uring", "test json-properties", "test resume-model", "rs quic-sim", "rs rung-disable", "test drill impaired", "rs cli-export", "rs hls-conformance", "rs quic-stress", "rs audio-devices", "rs multicast", "rs render-sw", "test qmux", "rs v4l2", "js worklet-matrix"] + recipe: ["gate", "gh test-integration", "rs doctest --workspace", "rs send-depth", "test drill-sensitivity", "rs uring", "test json-properties", "test resume-model", "test route-key-model", "rs quic-sim", "rs rung-disable", "test drill impaired", "rs cli-export", "rs hls-conformance", "rs quic-stress", "rs audio-devices", "rs multicast", "rs render-sw", "test qmux", "rs v4l2", "js worklet-matrix"] include: # Miri interprets kio's and moq-net's in-memory unsafe; too slow for the merge gate. - recipe: rs miri diff --git a/drafts/draft-lcurley-moq-lite.md b/drafts/draft-lcurley-moq-lite.md index f026f67e54..7609ffe2f5 100644 --- a/drafts/draft-lcurley-moq-lite.md +++ b/drafts/draft-lcurley-moq-lite.md @@ -38,6 +38,7 @@ normative: informative: I-D.lcurley-moq-cluster: + RFC7627: RFC8966: moqflate: title: "DEFLATE Compressed Tracks for MoQ" @@ -1069,8 +1070,10 @@ The sender's Ed25519 public key. The key's Ed25519 signature over the ASCII bytes `moq-lite route key`, then one byte naming the sender's side of the session (0 for the client, 1 for the server), then 32 bytes of keying material exported from the session with the label `EXPORTER-moq-lite-route-key` and an empty context. Binding 1 exports with the TLS exporter (Section 7.5 of [RFC8446]), and binding 2 with the WebTransport session's exporter [webtrans-h3] (see [Transports](#transports)). -An endpoint MUST NOT send the parameter on a session that provides no exporter. -The exported material and the sender's side keep a proof from being replayed on another session or reflected back to its sender. +The exporter MUST yield material that only the session's two endpoints know and no other session shares. +TLS 1.3's exporter provides this, after resumption too; its early exporter does not, since a replayed 0-RTT ClientHello reproduces it on another connection, nor does TLS 1.2 without the extended master secret [RFC7627], which lets an attacker give two of its sessions one secret. +An endpoint MUST NOT send the parameter on a session that provides no such exporter. +The exported material and the sender's side keep a proof from being replayed on another session, relayed by an attacker or an intermediary that terminates TLS, or reflected back to its sender. Either endpoint MAY send it. A receiver MUST close the session with a PROTOCOL_VIOLATION if the value is not 96 bytes. A receiver that relies on the key MUST verify the signature first, closing the session with a PROTOCOL_VIOLATION if it does not verify; without an exporter on the session, it cannot rely on the key. diff --git a/quest/m1/route-key-model.md b/quest/m1/route-key-model.md deleted file mode 100644 index 5c692d265e..0000000000 --- a/quest/m1/route-key-model.md +++ /dev/null @@ -1,55 +0,0 @@ -# [M] A symbolic model proves a route key proof binds to its session and side - -## Goal - -A Tamarin model of lite-07's Route Key Parameter proves that when an endpoint -accepts a key on a session, the holder of that key signed for that session -and that side of it. The attacker controls the network, runs its own sessions -with both endpoints, and holds other route keys. The draft states what each -transport binding's exporter must guarantee for the proof to hold, each -binding in Rust and JS is checked against that, and the model runs in Nightly. - -## Plan - -Decided 2026-11-10 (maintainer, /quest-plan on what could be proved about -moq-net): - -- ✅ Tamarin (rejected: no formal analysis; the proof is a hand-rolled - construction, the kind symbolic provers find reflection and relaying - attacks in). -- ✅ m1 and it gates the cut (rejected: ungated like the TLA+ models; m4). - The signed transcript freezes when lite-07 is cut, and a flaw in it can - only be fixed on the wire, so - [Finalize moq-lite-07](/quest/m2/lite07-finalize.md) lists this quest. - -The proof (`rs/moq-net/src/route/proof.rs`, `js/net/src/lite/`, the draft's -Route Key Parameter section) is an Ed25519 signature over the domain string, -one byte for the sender's side, and 32 bytes exported from the session. - -- Model the handshake as a session whose exporter secret only its two - endpoints know and no other session shares. That assumption is the result - to pin down: state it in the draft, then check each binding against it. - Cover at least TLS 1.3 only (an older TLS without extended master secret - lets one party give two sessions the same secret), resumption and 0-RTT, the - WebTransport session exporter, and a session reached through an intermediary - that terminates TLS. -- Lemmas: the protocol can run; an accepted proof implies its key's holder - signed on that session as that side (injective agreement); no reflection to - the sender; no replay on another session; a proof the attacker relays - between two sessions it terminates is rejected. -- Out of scope: an endpoint whose own key is compromised, and relays that - share one key on purpose, which the draft allows. -- A lemma that fails is a finding: fix the transcript in Rust, JS, and the - draft in this PR when the fix is clear, and bring the maintainer the wire - change when it is not. -- Keep the model beside the others (`rs/moq-net/verify/`), with a `verify-*` - skill in their shape and Tamarin run from the flake as the `tla` recipe - runs TLC. - -Public API: none unless a finding changes the proof. Wire: none unless a -finding changes the signed transcript. - -## Related - -- [The TLA+ models run nightly and reviews resync them](/quest/m1/model-checks-nightly.md) - the Nightly job and Coverage-table check this model joins -- [Routes and announces](/quest/m2/cluster-routing/routes/README.md) - files a peer's routes under the key this proves diff --git a/quest/m2/lite07-finalize.md b/quest/m2/lite07-finalize.md index d1dc62c499..d561b06a2c 100644 --- a/quest/m2/lite07-finalize.md +++ b/quest/m2/lite07-finalize.md @@ -134,7 +134,6 @@ transcript freezes at the cut and a flaw in it can only be fixed on the wire. - [Delete the old start bookkeeping](/quest/m2/subscribe-ranges/start-bookkeeping.md) - may change START per update on lite-07 - [Prove cache-aware routing](/quest/m2/cache-routing-proof.md) - may add the warm-route message to lite-07; leaves this list if the proof places it in a SETUP extension - [Route latency](/quest/m2/route-latency.md) - may add a latency sum to ROUTE; leaves this list if the maintainer takes the no-wire path -- [A symbolic model proves a route key proof binds to its session and side](/quest/m1/route-key-model.md) - may change what the Route Key Parameter signs, if the model finds a replay, reflection, or relaying attack ## Related diff --git a/rs/justfile b/rs/justfile index 391e57fb7c..6371163758 100644 --- a/rs/justfile +++ b/rs/justfile @@ -23,6 +23,11 @@ default: tla spec *args: nix shell --inputs-from . nixpkgs#tlaplus --command tlc -workers auto -cleanup -metadir "$(mktemp -d)" {{ args }} rs/{{ spec }} +# Prove a Tamarin model's lemmas, e.g. `just rs tamarin moq-net/verify/route-key/RouteKey.spthy`. +# Pass `-D=` for a variant the model defines. +tamarin spec *args: + nix shell --inputs-from . nixpkgs#tamarin-prover --command tamarin-prover --prove {{ args }} rs/{{ spec }} + # Default features for the selected packages; `features` covers the feature # matrix nightly and on release PRs. No `cargo check` pass: clippy is a # superset of it, and the two use different rustc wrappers, so running both diff --git a/rs/moq-net/verify/route-key/RouteKey.spthy b/rs/moq-net/verify/route-key/RouteKey.spthy new file mode 100644 index 0000000000..3f48aaf55a --- /dev/null +++ b/rs/moq-net/verify/route-key/RouteKey.spthy @@ -0,0 +1,206 @@ +theory RouteKey +begin + +/* + * lite-07's Route Key Parameter (`rs/moq-net/src/route/proof.rs`): an endpoint signs the + * domain, its side of the session, and 32 bytes exported from the session's handshake, so a + * peer files its routes under that key. + * + * The attacker owns the network, runs sessions of its own with every endpoint, and makes + * route keys of its own. Each honest endpoint holds one key that never leaks. A session's + * exporter derives from its connection's secret, which only that connection's two ends hold + * (TLS 1.3, RFC 8446 section 7.5): binding 1 exports it directly, and binding 2 under the + * WebTransport session's ID (draft-ietf-webtrans-http3 section 4.8). + * + * Every run records the endpoint really at its other end, `'adv'` for the attacker, so the + * lemmas say what a proof means without trusting what an endpoint believes. + * + * Each variant drops one assumption the draft states and must break exactly the lemmas its + * `Breaks:` line names; `test/route-key-model.sh` checks that, so the model stays sharp. + * + * NO_SIDE Breaks: no_relay no_reflection injective_agreement + * The signature leaves out the sender's side, so the attacker hands an endpoint's + * proof back to it. + * EARLY Breaks: no_replay injective_agreement + * A resumed session exports from its 0-RTT secret, which a replayed ClientHello + * reproduces on another connection. + * NO_EMS Breaks: no_relay no_reflection injective_agreement + * A man in the middle gives its two sessions one secret, as TLS 1.2 without the + * extended master secret (RFC 7627) allows, and relays between them, even from an + * endpoint to itself. + */ + +builtins: signing, hashing + +restriction once: + "All x #i #j. Once(x) @ #i & Once(x) @ #j ==> #i = #j" + +restriction verified: + "All a b #i. Eq(a, b) @ #i ==> a = b" + +// `'adv'` names the attacker's end of a session, never an endpoint. +restriction endpoint: + "All e #i. Endpoint(e) @ #i ==> not (e = 'adv')" + +// One route key per endpoint: relays sharing a key on purpose are out of scope. +rule Key: + [ Fr(~sk) ] + --[ Endpoint($E), Once(<'key', $E>), KeyOf($E, pk(~sk)) ]-> + [ !Ltk($E, ~sk), Out(pk(~sk)) ] + +/* Connections. `$b` is the binding: 'quic' (1) or 'h3' (2). */ + +// A full TLS 1.3 handshake between two endpoints, or an endpoint and itself. +rule Connect: + [ Fr(~conn), Fr(~ms) ] + --[ Endpoint($C), Endpoint($S) ]-> + [ !End(~conn, $C, 'client', $S, ~ms, $b), !End(~conn, $S, 'server', $C, ~ms, $b) ] + +// An endpoint dials the attacker, or an intermediary that terminates TLS. +rule Connect_to_adv: + [ Fr(~conn), Fr(~ms) ] + --[ Endpoint($C) ]-> + [ !End(~conn, $C, 'client', 'adv', ~ms, $b), Out(~ms) ] + +// The attacker, or an intermediary that terminates TLS, dials an endpoint. +rule Connect_from_adv: + [ Fr(~conn), Fr(~ms) ] + --[ Endpoint($S) ]-> + [ !End(~conn, $S, 'server', 'adv', ~ms, $b), Out(~ms) ] + +// Resumption: the new secret mixes the PSK with fresh handshake randoms, even without +// (EC)DHE, and the session exports only once the handshake completes. +rule Resume: + [ !End(conn, C, 'client', S, ms, b), !End(conn, S, 'server', C, ms, b), Fr(~conn2), Fr(~n) ] + --> + [ Out(~n), + !End(~conn2, C, 'client', S, h(<'resumption', ms, ~n>), $b2), + !End(~conn2, S, 'server', C, h(<'resumption', ms, ~n>), $b2) ] + +#ifdef EARLY +// The client sends its SETUP in 0-RTT, signing over the early secret... +rule Resume_early_client: + [ !End(conn, C, 'client', S, ms, b), !End(conn, S, 'server', C, ms, b), Fr(~conn2), Fr(~hello) ] + --> + [ Out(~hello), !End(~conn2, C, 'client', S, h(<'early', ms, ~hello>), $b2) ] + +// ...and the server derives it from whichever ClientHello arrives, replays included. +rule Resume_early_server: + [ !End(conn, S, 'server', C, ms, b), In(hello), Fr(~conn3) ] + --> + [ !End(~conn3, S, 'server', C, h(<'early', ms, hello>), $b2) ] +#endif + +#ifdef NO_EMS +// The triple handshake: one secret on the attacker's session with each endpoint. +rule Synchronize: + [ Fr(~conn1), Fr(~conn2), Fr(~ms) ] + --[ Endpoint($C), Endpoint($S) ]-> + [ !End(~conn1, $C, 'client', 'adv', ~ms, $b), + !End(~conn2, $S, 'server', 'adv', ~ms, $b), + Out(~ms) ] +#endif + +/* Sessions: each end of a connection derives the session's exporter itself. */ + +// Binding 1: one session per connection, exporting from the connection. +rule Session_quic: + [ !End(conn, E, side, peer, ms, 'quic'), Fr(~r) ] + --[ Once(<'session', conn, E, side>) ]-> + [ !Run(~r, E, side, peer, h(<'exporter', ms, 'EXPORTER-moq-lite-route-key'>)) ] + +// Binding 2: WebTransport sessions share a connection, each exporting under its own ID, +// which the attacker picks, but never twice on one connection. +rule Session_webtransport: + [ !End(conn, E, side, peer, ms, 'h3'), In(id), Fr(~r) ] + --[ Once(<'session', conn, E, side, id>) ]-> + [ !Run(~r, E, side, peer, + h(<'exporter', ms, 'EXPORTER-WebTransport', >)) ] + +/* The proof: SETUP's Route Key Parameter, sent and checked once per session. */ + +#ifdef NO_SIDE +rule Prove: + [ !Run(r, E, side, peer, ex), !Ltk(E, sk) ] + --[ Once(<'prove', r>), Signed(E, peer, pk(sk), side, ex) ]-> + [ Out(, sk)>) ] + +rule Accept_from_server: + [ !Run(r, E, 'client', peer, ex), In() ] + --[ Once(<'accept', r>), Eq(verify(sig, <'moq-lite route key', ex>, k), true), + Accepted(r, E, peer, k, 'server', ex) ]-> + [ ] + +rule Accept_from_client: + [ !Run(r, E, 'server', peer, ex), In() ] + --[ Once(<'accept', r>), Eq(verify(sig, <'moq-lite route key', ex>, k), true), + Accepted(r, E, peer, k, 'client', ex) ]-> + [ ] +#else +rule Prove: + [ !Run(r, E, side, peer, ex), !Ltk(E, sk) ] + --[ Once(<'prove', r>), Signed(E, peer, pk(sk), side, ex) ]-> + [ Out(, sk)>) ] + +rule Accept_from_server: + [ !Run(r, E, 'client', peer, ex), In() ] + --[ Once(<'accept', r>), Eq(verify(sig, <'moq-lite route key', 'server', ex>, k), true), + Accepted(r, E, peer, k, 'server', ex) ]-> + [ ] + +rule Accept_from_client: + [ !Run(r, E, 'server', peer, ex), In() ] + --[ Once(<'accept', r>), Eq(verify(sig, <'moq-lite route key', 'client', ex>, k), true), + Accepted(r, E, peer, k, 'client', ex) ]-> + [ ] +#endif + +/* Lemmas */ + +// Two endpoints accept each other's keys over raw QUIC. +lemma executable: + exists-trace + "Ex a b ka kb ex r1 r2 #i #j #k #l. + KeyOf(a, ka) @ #k & KeyOf(b, kb) @ #l & not (a = b) + & Accepted(r1, a, b, kb, 'server', ex) @ #i + & Accepted(r2, b, a, ka, 'client', ex) @ #j" + +// The same after resumption, over a WebTransport session. +lemma executable_resumed_webtransport: + exists-trace + "Ex a b ka ms n id r #i #k. + KeyOf(a, ka) @ #k & not (a = b) + & Accepted(r, b, a, ka, 'client', + h(<'exporter', h(<'resumption', ms, n>), 'EXPORTER-WebTransport', + >)) @ #i" + +// An honest key is never accepted on a session the attacker or an intermediary terminates, +// even when it relays the proof live from its session with the key's holder. +lemma no_relay: + "All r e k side ex #i a #h. + Accepted(r, e, 'adv', k, side, ex) @ #i & KeyOf(a, k) @ #h ==> F" + +// An endpoint accepts its own key only from itself, as the other side: the attacker never +// reflects the endpoint's proof back to it. +lemma no_reflection: + "All r e peer k side ex #i #h. + Accepted(r, e, peer, k, side, ex) @ #i & KeyOf(e, k) @ #h + ==> peer = e & (Ex #j. Signed(e, e, k, side, ex) @ #j & #j < #i)" + +// One signature is accepted on one session only: never replayed onto another. +lemma no_replay: + "All r1 r2 e1 e2 p1 p2 k side ex a #i #j #h. + Accepted(r1, e1, p1, k, side, ex) @ #i & Accepted(r2, e2, p2, k, side, ex) @ #j + & KeyOf(a, k) @ #h + ==> r1 = r2" + +// Injective agreement: an accepted honest key was signed by its holder, who is the +// session's other end, for that side of that session, and no other session accepts it. +lemma injective_agreement: + "All r e peer k side ex a #i #h. + Accepted(r, e, peer, k, side, ex) @ #i & KeyOf(a, k) @ #h + ==> peer = a + & (Ex #j. Signed(a, e, k, side, ex) @ #j & #j < #i) + & not (Ex r2 e2 p2 #i2. Accepted(r2, e2, p2, k, side, ex) @ #i2 & not (r2 = r))" + +end diff --git a/test/justfile b/test/justfile index d7a8b4deaa..de86aeaa78 100644 --- a/test/justfile +++ b/test/justfile @@ -294,6 +294,10 @@ json-properties: resume-model: bash ../sh/local.sh bash resume-model.sh +# Prove the route key model, and that each variant breaks the lemmas it names. +route-key-model: + bash route-key-model.sh + # The TypeScript qmux peer as client and server against the in-tree Rust qmux # interop examples, per draft. The manifest path names the in-tree crate, which # shares its package name with the 0.6 release its tests interoperate with. diff --git a/test/route-key-model.sh b/test/route-key-model.sh new file mode 100755 index 0000000000..839e540f41 --- /dev/null +++ b/test/route-key-model.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash +# Prove the route key model, then check each variant breaks exactly the lemmas its +# `Breaks:` line names. Tamarin exits 0 whatever it finds, so this reads its summary. +set -euo pipefail +cd "$(git rev-parse --show-toplevel)" + +spec=moq-net/verify/route-key/RouteKey.spthy +log=$(mktemp -d) +trap 'rm -rf "$log"' EXIT + +failed=() +check() { + local name=$1 breaks=$2 + shift 2 + local status=0 + just rs tamarin "$spec" "$@" > "$log/$name" 2>&1 || status=$? + if [ "$status" -ne 0 ]; then + cat "$log/$name" + failed+=("$name: tamarin exited $status") + return + fi + if grep -q 'wellformedness check failed' "$log/$name"; then + failed+=("$name: not wellformed") + fi + local lemmas + lemmas=$(grep -E '^ [a-z_]+ \((all|exists)-traces?\): ' "$log/$name" || true) + echo "== $name" + echo "$lemmas" + [ -n "$lemmas" ] || failed+=("$name: no lemma results") + while read -r lemma _ result _; do + [ -n "$lemma" ] || continue + local want=verified + [[ " $breaks " != *" $lemma "* ]] || want=falsified + [ "$result" = "$want" ] || failed+=("$name: $lemma is $result, want $want") + done <<< "$lemmas" +} + +check base "" +while read -r variant _ breaks; do + check "$variant" "$breaks" "-D=$variant" +done < <(sed -nE 's/^ \* ([A-Z_]+) +Breaks: (.*)$/\1 Breaks: \2/p' "rs/$spec") + +if [ ${#failed[@]} -ne 0 ]; then + printf 'error: %s\n' "${failed[@]}" >&2 + exit 1 +fi From 83bcddb79985aa7870eb0342146fa05888b6e0cc Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 01:10:34 -0800 Subject: [PATCH 3/6] test: shfmt the route key model runner Co-Authored-By: Claude Opus 5.5 --- test/route-key-model.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/route-key-model.sh b/test/route-key-model.sh index 839e540f41..0c3bce9669 100755 --- a/test/route-key-model.sh +++ b/test/route-key-model.sh @@ -13,7 +13,7 @@ check() { local name=$1 breaks=$2 shift 2 local status=0 - just rs tamarin "$spec" "$@" > "$log/$name" 2>&1 || status=$? + just rs tamarin "$spec" "$@" >"$log/$name" 2>&1 || status=$? if [ "$status" -ne 0 ]; then cat "$log/$name" failed+=("$name: tamarin exited $status") From c6ca85795199679cf5b706089aad7b1b49dacb02 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 01:16:41 -0800 Subject: [PATCH 4/6] test: shfmt the route key model runner's here-string Co-Authored-By: Claude Opus 5.5 --- test/route-key-model.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/route-key-model.sh b/test/route-key-model.sh index 0c3bce9669..0a74fad8c9 100755 --- a/test/route-key-model.sh +++ b/test/route-key-model.sh @@ -32,7 +32,7 @@ check() { local want=verified [[ " $breaks " != *" $lemma "* ]] || want=falsified [ "$result" = "$want" ] || failed+=("$name: $lemma is $result, want $want") - done <<< "$lemmas" + done <<<"$lemmas" } check base "" From 20ccfeedd0993113620957b377896874b55606f8 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 11:04:41 -0800 Subject: [PATCH 5/6] test(net): route key model checks both resumed proofs and fails on unparsed variants The resumed WebTransport lemma now requires both endpoints to accept each other's proof. The script fails when no variant is found, when a variant's lemma set differs from the base's, or when a Breaks: name has no result. Co-Authored-By: Claude Opus 5.5 --- rs/moq-net/verify/route-key/RouteKey.spthy | 11 +++++++---- test/route-key-model.sh | 21 ++++++++++++++++++--- 2 files changed, 25 insertions(+), 7 deletions(-) diff --git a/rs/moq-net/verify/route-key/RouteKey.spthy b/rs/moq-net/verify/route-key/RouteKey.spthy index 3f48aaf55a..3252f1c134 100644 --- a/rs/moq-net/verify/route-key/RouteKey.spthy +++ b/rs/moq-net/verify/route-key/RouteKey.spthy @@ -168,11 +168,14 @@ lemma executable: // The same after resumption, over a WebTransport session. lemma executable_resumed_webtransport: exists-trace - "Ex a b ka ms n id r #i #k. - KeyOf(a, ka) @ #k & not (a = b) - & Accepted(r, b, a, ka, 'client', + "Ex a b ka kb ms n id r1 r2 #i #j #k #l. + KeyOf(a, ka) @ #k & KeyOf(b, kb) @ #l & not (a = b) + & Accepted(r1, a, b, kb, 'server', + h(<'exporter', h(<'resumption', ms, n>), 'EXPORTER-WebTransport', + >)) @ #i + & Accepted(r2, b, a, ka, 'client', h(<'exporter', h(<'resumption', ms, n>), 'EXPORTER-WebTransport', - >)) @ #i" + >)) @ #j" // An honest key is never accepted on a session the attacker or an intermediary terminates, // even when it relays the proof live from its session with the key's holder. diff --git a/test/route-key-model.sh b/test/route-key-model.sh index 0a74fad8c9..4915deee4a 100755 --- a/test/route-key-model.sh +++ b/test/route-key-model.sh @@ -9,6 +9,7 @@ log=$(mktemp -d) trap 'rm -rf "$log"' EXIT failed=() +base_names="" check() { local name=$1 breaks=$2 shift 2 @@ -23,10 +24,21 @@ check() { failed+=("$name: not wellformed") fi local lemmas - lemmas=$(grep -E '^ [a-z_]+ \((all|exists)-traces?\): ' "$log/$name" || true) + lemmas=$(grep -E '^ [A-Za-z0-9_]+ \((all|exists)-traces?\): ' "$log/$name" || true) echo "== $name" echo "$lemmas" [ -n "$lemmas" ] || failed+=("$name: no lemma results") + local names + names=$(awk '{print $1}' <<<"$lemmas" | sort | tr '\n' ' ') + if [ -z "$base_names" ]; then + base_names=$names + elif [ "$names" != "$base_names" ]; then + failed+=("$name: lemmas are [$names], want the base's [$base_names]") + fi + local expected + for expected in $breaks; do + [[ " $names" == *" $expected "* ]] || failed+=("$name: breaks $expected, which has no result") + done while read -r lemma _ result _; do [ -n "$lemma" ] || continue local want=verified @@ -36,9 +48,12 @@ check() { } check base "" -while read -r variant _ breaks; do +variants=$(sed -nE 's/^ \* ([A-Z_]+) +Breaks: (.*)$/\1 \2/p' "rs/$spec") +[ -n "$variants" ] || failed+=("no variant has a Breaks: line") +while read -r variant breaks; do + [ -n "$variant" ] || continue check "$variant" "$breaks" "-D=$variant" -done < <(sed -nE 's/^ \* ([A-Z_]+) +Breaks: (.*)$/\1 Breaks: \2/p' "rs/$spec") +done <<<"$variants" if [ ${#failed[@]} -ne 0 ]; then printf 'error: %s\n' "${failed[@]}" >&2 From 6a27cacc7b529541dedd3bb263cff9a7cfb2e5ed Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 11:24:57 -0800 Subject: [PATCH 6/6] test(net): every #ifdef in the route key model needs a parsed Breaks: line Co-Authored-By: Claude Opus 5.5 --- test/route-key-model.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/test/route-key-model.sh b/test/route-key-model.sh index 4915deee4a..e5ad887671 100755 --- a/test/route-key-model.sh +++ b/test/route-key-model.sh @@ -48,8 +48,11 @@ check() { } check base "" -variants=$(sed -nE 's/^ \* ([A-Z_]+) +Breaks: (.*)$/\1 \2/p' "rs/$spec") -[ -n "$variants" ] || failed+=("no variant has a Breaks: line") +variants=$(sed -nE 's/^ \* ([A-Za-z0-9_]+) +Breaks: (.*)$/\1 \2/p' "rs/$spec") +# Every #ifdef is a variant, so a header that stops parsing cannot retire its negative control. +while read -r variant; do + grep -q "^$variant " <<<"$variants" || failed+=("$variant: no Breaks: line") +done < <(sed -nE 's/^#ifn?def ([A-Za-z0-9_]+).*/\1/p' "rs/$spec" | sort -u) while read -r variant breaks; do [ -n "$variant" ] || continue check "$variant" "$breaks" "-D=$variant"