Proving nfltr's end-to-end encryption against a hostile relay

November 8, 2026

nfltr moves your traffic through a relay: your machines dial out to it, and it connects them to each other, to a browser or to a phone. "End-to-end encrypted" should mean that whoever runs that relay, or takes it over, can pass your traffic along but can neither read it nor change it. That is easy to claim and hard to check, so we proved it, path by path, against a relay that lies.

Updated 2026-11-09

After publishing, we reviewed every claim in this post against the code, as an attacker would. Most claims held. Where they didn't, we fixed the code or the text, and we list everything we found here rather than editing silently:

Fixed in code (on main, shipping in the next release): agent-to-agent key choice that a relay could steer to a leaked machine's key (K1 to K3 in the findings); a WireGuard or P2P end holding the root key file that trusted the relay's word for which machine it reached (K4); a second nonce-reuse path in peer-to-peer data records; and share links that said "Verified" while the relay ended their TLS.
Text corrected: a revocation made in the account, rather than on the hub's machine, reaches agent-to-agent calls within 5 minutes. A pinned TCP session the relay cuts between TLS records reads as a clean end.

What this means for you

What you get. On an end-to-end encrypted path the relay forwards bytes it can't read or change, and it can't send them to a machine you didn't choose. Only your two ends hold the keys.
Where you get it:
- calls between your hub and your machines: always on, nothing to switch on; and messages from a phone or browser you paired with your hub;
- tcp services through nfltr dial, tcp-connect, ssh-proxy or a connect: mapping, with a pin;
- WireGuard (nfltr wg) and peer-to-peer calls and file transfers (nfltr p2p), with a key file on both ends;
- end-to-end encrypted share links, for a visitor who checks your machine's certificate fingerprint.
What you do. Copy the fingerprint your agent prints into --pin (or pin:), and list each client's key on the agent (--allow-client; nfltr config client-key prints it). Give WireGuard and P2P a key file (--e2ee-key-file). Your hub makes its own key; each machine gets its key from nfltr node join, or as a file you copy to it. The first use is yours to protect: carry each fingerprint and key file yourself, never from a page the relay shows. A key that came through the relay, or no key file at all, means trusting the relay.
What isn't covered. Inspectable links (--mode inspectable, which share sign-in, recording and routes need): the relay ends TLS and sees each request, by design. A share link opened in a browser without that fingerprint check: the relay runs the share domain and could get a certificate for it. And on every path: who talks to whom, when and how much; a relay that refuses to carry anything; bugs in the code below the rules we proved.
Why you can trust this. Every path has a machine-checked proof in which the relay is the attacker, alone or with a second relay. The proofs found real attacks in shipped code, all fixed before this post, and the proofs of the relay's own paths are public: you can rerun them and break them on purpose.

The rest of this post is for developers and auditors: the attacker, the method, each path's model with its queries and planted mistakes, the attacks found and how each was fixed, what is assumed, what is not proven, what it costs per push, and how to rerun it.

A test suite exercises an honest relay; the bugs that matter here appear only when the relay lies. A hostile relay does much more than read: it hands each end the other's key, decides which machine a connection reaches, replays, drops, reorders or reflects messages, and runs the TURN server and the mailboxes that carry the rest. So since 2026-11-07 every end-to-end encrypted path in nfltr has a symbolic model, checked with ProVerif, in which the attacker is every relay. It is the companion of What TLA+ found in nfltr: TLA+ checks our state machines, ProVerif checks who can learn or forge what.

What the proofs found

Attacks in shipped code, each fixed before this post: an agent that sent decrypted traffic wherever the relay named; an agent service that any relay could reach; agent-to-agent calls a relay could reroute, reflect, replay or cut short; a hub page that showed an accepted approval as refused; an encryption nonce used twice.
Found by TLA+ and by traces of the code: a retry that ran one request twice (in the design, before the code), a key rotation that did the same, and a cancel sent for a call that never reached its target (both in the code, by checking recorded runs against the spec).
What holds now: on every path, against two colluding relays, the payload stays secret and each end agrees on who it talks to, once the first key reached it out of band.
The limits: the first use of a key, metadata, side channels and the code below the modelled rules.
The cost: 73 ProVerif runs on every push, across the CI of four repositories. A run is one model, one of its variants, or one planted mistake, so these are not 73 separate proofs. They take 284 to 322 s per push in the relay repository and seconds in the others.

Contents: at a glance · the attacker · the method · the paths · agent to agent · two relays · what it found · what is assumed · what is not proven · cost · rerun it · fit

At a glance

For security reviewers: what holds and what doesn't, each row detailed further down.

if this happens	what the attacker gets
a relay is hostile, or two relays collude	nothing on an end-to-end path: payloads stay secret and each end agrees on who it talks to (the paths, two relays)
a relay reroutes a session to another of your machines	a refused handshake: the callee, exit or responder is bound into the keys (findings F3 and 5). A WireGuard client or P2P caller holding the root key file takes only the machine it named, from its own store (finding K4, fixed after v2.1.54)
a relay replays, reflects, reorders or cuts short A2A frames	refused (A2A queries 7 to 10 and 16 to 18). For pinned TCP, TLS refuses replay, reflection and reordering, but a stream the relay cuts between two TLS records reads as a clean end (Go's TLS accepts an end without close_notify there): only the application's own framing notices it
one machine's key leaks	that machine's own traffic; no other machine's calls (A2A), and no exit or session of a client holding another machine's key file. Until the release after v2.1.54, a relay holding one leaked machine key could also read the hub's calls to another machine (findings K1 to K3), and sit in the middle of a WireGuard or P2P session of a client holding the root key file (K4)
the hub's root key leaks later	past A2A calls stay secret (forward secrecy holds in the model). Treat every machine key it made as leaked from then on
a client key or machine is revoked	a machine revoked on the hub's machine (`nfltr orch hub machines revoke`): its A2A calls end at once. One revoked in the account (dashboard, `nfltr machines revoke`): the relay ends its connections, and the hub's A2A keys follow within 5 minutes, read through the relay, which a hostile relay can withhold. A removed client key is refused from the agent's next start, while a session already running continues (limits)
the first key or fingerprint comes through the relay	everything: the relay can sit in the middle. Carry it yourself (limits)
the A2A callee restarts right after a resumed call	the relay can make that call run twice (gap L1, limits)
the relay watches traffic or refuses to carry it	who talks to whom, when and how much; a denial of service. Not covered
the code differs from the model below the modelled rules	not excluded by a proof; tied by citations, wire vectors and tests (limits)

The attacker

One attacker plays every relay. It holds the relays' certificate authority, so it can issue a certificate for any machine to any relay. It reads, drops, delays, reorders, replays and forges every message it carries, writes every connect label and routing id, and runs the TURN server and the mailboxes. When the two ends sit on different relays (two replicas today, separate relays later), it owns both and the link between them, and can reroute a session to a third machine of the same owner. It may also hold the keys of some of the owner's machines: leaked, or revoked.

In plain words: everything between your two machines may be the attacker's; only the two ends are trusted.

What the relay may still do, and no model claims otherwise: refuse to carry anything (denial of service), and see who talks to whom, when, and how much.

The method

ProVerif works in the symbolic (Dolev-Yao) model. Messages are terms; encryption opens only with its key; Diffie-Hellman has its one equation; hashes, HMAC and HKDF are free functions. The attacker computes anything it can from what it has seen. Against that attacker each model states two kinds of query:

Secrecy: the attacker never learns this payload or this key.
Agreement: when one end accepts a message as the other's, the other sent it, in this session, with these keys, to this target. "Injective" adds: once (no replay).

Three rules keep the results honest:

Witnesses. Every model also asks whether the honest flow completes at all. Those queries must fail (ProVerif finds the flow); a model where nothing ever completes would prove everything.
Mutants. Each check the code makes has a flag that removes it again: skip the pin, take the key from the relay, fall back to plaintext, drop a field from the transcript. With the flag on, the query that check protects must fail with an attack trace. expect.txt lists every model, flag and result in query order (T holds, F attack, ? not proved), and run.sh fails when any line differs.
Citations. Every rule of a model cites the file and line of the code it models; a code map in each README lists those files, and a drift check fails a push that changes one of them without the model (or a stated reason why the model still holds). Each finding also has a Go test that fails on the old code.

We do not re-prove the standard protocols underneath. TLS 1.3, WireGuard's Noise handshake, DTLS-SRTP and SSH are each assumed to be an authenticated channel to whoever holds the key the other end checked, as their published proofs show (below). What we prove is ours: how each end learns the other's key, what it checks, which name or target it binds, and every place a relay could steer it to something weaker.

The paths

Eight models cover the paths. Each diagram shows who holds which key, and what the relay sees.

Pinned TCP sessions

nfltr dial, tcp-connect and ssh-proxy with --pin (or pin: on a connect: mapping) run TLS with the agent inside the relay's session. The client checks the agent's certificate against the fingerprint the agent printed; the agent asks for the client's own key and serves only the keys it lists (nfltr tcp <port> --allow-client, allow_client: in nfltr up).

In plain words: the client and the agent each check the other's key; the relay carries records it can't open and learns only which agent, when and how much.

Model e2ee_tcp.pv (public, relay repository). Queries: the payload is secret (1); a response the client accepts came from the pinned key in that session, once (2); an end-to-end nfltr tcp without --forward stays secret (3, finding 1 below); after a rotation, a client pinned to the new certificate is safe (4), one still pinned to the old one is not (5, documented: re-pin); a pin taken from anything the relay shows is not (6, documented); the agent's service against the relay (7, finding 2); a removed client key reaches nothing (8); what reaches the service was sent by the allowed client (9); witness (10). Mutants: skip the pin check, a relay-supplied pin, plaintext when the relay gives no answer, the relay's target without --forward, the relay's target despite --forward, accept a response without the session key, accept any client certificate, skip the client's CertificateVerify.

The client check is a mirror of the server pin:

In plain words: each end stops unless the other shows the key it expects: the client its pin, the agent a client key on its list.

WireGuard

nfltr wg makes the client and the exit WireGuard peers of each other; the relay forwards sealed packets and holds no WireGuard key. It does hand each side the other's public key, so on its own the relay could put itself in the middle. With a pairing key (--e2ee-key-file) both ends mix a preshared key into every handshake: HMAC over the exit's A2A key (the owner's root key, or the machine key of the exit's machine), the exit's service name and the key id.

In plain words: both ends mix in a secret from your key file, so a relay that swaps the public keys can't finish the handshake.

Model wg_exit.pv (relay). Paired: the payload is secret unless the machine the client named is leaked (1); injective agreement of the exit with the client on the exit's name, the machine named, both keys and payload, with an exit of the same name on a second machine (2); two exits on one machine key, a client rerouted to the other is refused (4, finding 5); a leaked machine key reaches no other machine's exit (5); the key id a client used is the machine it named (6, finding K4); witnesses (7, 8). Unpaired: the payload is not secret (3, documented: the relay hands each end its own key). Mutants: drop the preshared key on the relay's word, none at the client, none at the exit, one key for all machines, the name left out of the key, the relay's key id taken (K4). A second model, in the relay server repository (private), checks the honest relay's part without a pairing key: another account's clients and exits, one named like yours, never get your payload (2 queries, 2 mutants).

Peer-to-peer calls and transfers

nfltr p2p connects two machines directly (or through TURN), signalled through the relay. With a key file on both, the signalling is sealed and the HKDF salt of the session is bound to the pair's key, the responder's name and the pair's key id. The browser call page carries its DTLS fingerprint inside a sealed signalling frame, so media is covered too.

In plain words: the setup messages are sealed with your key file, so the relay and the TURN server move only packets they can't open.

Model p2p_e2e.pv (relay). Paired: data secret unless the pair key id is a leaked machine's (1); browser media secret (2); injective agreement of the responder with the initiator on its name, key id, session id, keys and data (3, finding 5); agreement on the key confirmation (4); a root initiator's data secret unless the machine it named is leaked, the key id it used is that machine, and a responder of the same name on another machine gets none of it (7-9, finding K4); witnesses (10-12). Unpaired: data not secret (5, documented), but equal fingerprints shown on both machines mean the same two keys (6: symbolically; computationally an 80-bit second preimage). Mutants: no pairing salt, skip the responder's confirmation, the old protocol in plaintext, accept any DTLS fingerprint, an unsealed SDP, fingerprints not compared, one key for all machines, the name left out of the salt, the relay's key id taken (K4).

End-to-end encrypted share links

An end-to-end encrypted share ends TLS at the agent; the relay routes by the name in the TLS ClientHello. A share with a credential must reach only an agent stream that checks it, on whichever replica the visitor came in.

In plain words: the visitor's encryption ends at your machine and your agent checks the share's password or token; a visitor who skips the fingerprint check is still trusting the relay.

Model e2ee_share.pv (public, relay-core repository). Part one, the relay honest, the attacker every visitor: the backend behind a credentialed share is reached only with the credential, on either replica (1). Part two, the relay hostile: a browser that trusts the share's WebPKI certificate is not protected (2, documented: the relay runs the share domain, its DNS and every ACME challenge, and issued the credential). Only the visitor checking the agent's own fingerprint (the one the agent prints) keeps that relay out; no nfltr command makes that check for a share link yet, which is why the pinned path above is the one to use against a hostile relay. Mutants: the gate skipped on the local path, skipped on a session the replica link brought, the share not carried on the link, the agent skipping the credential.

The hub's paired devices

The owner's browser, paired with a hub, sends messages and approvals end to end through the relay's mailboxes, and reads the hub's sections. Model hubremote.pv (nfltr repository, private) holds: a device's messages are secret (1); pairing through the link's secret (2); what the hub accepts was sent by that pinned device, for that hub (3); an approval the hub applies was given by the owner's passkey on that request (4); a section the device accepts was published by its hub (5); a message the device shows as refused was refused by the hub (6, finding 3); with a hostile page after an honest pairing, every applied approval took a tap (7); witness (10). Documented attacks: the tap need not be on that request when the page is hostile (8), and the page the relay serves at pairing can pair keys of its own (9). Mutants: skip the pairing MAC, an unsigned hub key, skip the envelope signature, an unsigned section, skip the passkey step-up, and finding 3 put back on each side.

In plain words: your device and your hub sign and seal every message; the relay's mailboxes only store and order them.

Agent to agent

A hub calls the agents it runs on other machines over the relay: agent to agent (A2A). This is where the models found the most.

The trust anchor

If A2A trusted the certificates the relays' CA issues, whoever runs that CA would be in the middle of every call. So A2A does not: the anchor is the owner's root key, which lives on the hub's machine and never leaves it. Each machine gets K_m = HKDF(K_root, machine id, generation), made on the hub's machine and carried to the machine by the owner (written in place by nfltr node join where the root is, or a file the owner copies), never through a relay. The relay's certificate authenticates a machine to the relay and carries its id; it never authenticates an A2A peer.

In plain words: one root key on the hub's machine makes a key for each machine; those keys never travel through a relay, and the relay's certificates never stand in for one.

Model a2a_keytransfer.pv (nfltr, private): the root key never leaves the hub's machine (1); a machine given its key file by the owner, and the hub's own node with an id the relay may name, each use a key the relay does not know (2, 3); witnesses (4, 5). Mutants: the key file sent through the relay, the root key copied to every machine (one leaked machine then leaks all), node join deriving for a relay-named id it already issued.

The handshake and sessions

Wire v2 is Noise NNpsk0 under a psk derived from the machine key, with a prologue that binds the call's transaction id, the initiator's role, the caller, the callee and the key id. The caller picks the key id from the agent it calls, so a relay that reroutes the call reaches a machine that cannot complete the handshake. Frames use one Noise cipher state per direction with counter nonces; the response's headers, the end of a stream and errors are sealed like data. There is no mode without a key: a command without its key refuses to start, and a keyed agent refuses every plaintext call.

One handshake per (hub, machine) pair is kept as a session: later calls resume it with a tagged first frame and send their request at once, each call under its own keys. No request ever rides the handshake's first message: sealed under the psk alone, it could be replayed. The relay client also has a warm-up, a handshake with no call so that a first call already resumes. It is in the models, but the hub does not use it in this release: measured on a 0.2 s relay round trip, it saved nothing.

In plain words: the first call proves that both ends hold the machine's key and keeps a session; later calls reuse it, each under keys of its own.

Model a2a_machine.pv (relay), 25 queries, checked with every relay and the link the attacker's, its CA the attacker's and two other machines (one revoked) leaked: secrecy of both directions both ways (1-4); the hub agrees with the machine it called on txn, keys and key id, injectively (5); the caller a hub accepts as machine m is m (6); each request is handled once (7, 8); no reflection (9); the end of a stream is the sender's (10); a revoked machine gets no frame and no handshake after the revoke (11, 12) and no resumed call (13); a session is its pair's (14); no nonce is used twice (15); no splice or replay across calls (16-18); response headers are the callee's (25); witnesses on handshake and resumed calls (19-24). A variant leaks the root key after the calls: forward secrecy of all of them holds. Mutants, each failing the queries it targets: drop-psk, relay-cert, drop-txn, no-target-check, drop-role, skip-revoke, one-key, clear-end, sess-unbound, txn-unbound, survive-revoke, counter-reset, warm-untyped, early-data, clear-header.

The one stateful part, a resumed call served at most once across the callee's replay window, restarts and retries, is a state property, so it is in TLA+: A2ASession.tla in the relay repository (AtMostOnce, NoKeyReuse, RevokeEnds, OnceRetry).

Two relays

A caller on relay X and a callee on relay Y: the models run each relay hostile alone, the link alone and all of them colluding (a relay's hops made private channels with an honest forwarder, the link always public, since a compromised relay holds its end of it).

In plain words: with two relays, one of them hostile or both, or only the link between them, every result is the same as with one; a call rerouted to another of your machines fails.

Every result is the same in every variant; no property holds only with one relay, and none is weaker with two. A reroute to a third machine is the attacker changing the routing id on its hop; wire v2 refuses it (query 5). One variant of the session model (only the link hostile) does not terminate in ProVerif and is not run; its results follow by monotonicity (making a channel private only takes capabilities from the attacker), and its witnesses are checked in the other variants.

What it found

Each finding below is fixed and has a Go test that fails on the old code. Those a model found are also mutants (the old code put back) that the model must catch on every push; S2's run is kept as a trace the checker must reject. Every fix ships in the release this post accompanies, except K1 to K4: found after it by checking the code against the models (the code did what a mutant does), they ship in the next release.

finding	the problem	how it was found	fix
F1 (A2A) reflection	return a frame to its sender, who opened it as the peer's: a caller read its own request as the response	ProVerif, wire v1 queries 7, 9	one key per direction (Noise cipher states)
F2 (A2A) no order, no sealed end	replay, drop or reorder frames, end a stream early as a clean end, forge a peer's error text	ProVerif query 8, then reading the code	counter nonces; END and ERROR sealed like data
F3 (A2A, high) callee not bound	reroute a call to another machine of the owner; with one leaked machine key, read what the hub sent to every machine	ProVerif, wire v1 queries 1, 6	the key id from the agent called, the callee checked in the prologue
F6 (A2A) reflection to the caller's own machine	return a machine's call to that machine, told it came from the hub	ProVerif, wire v2 before release	the initiator's role in the prologue
relay-named target (high)	an end-to-end `nfltr tcp` without `--forward` dialled the target the relay wrote, after decrypting: the plaintext went wherever the relay chose	ProVerif, `e2ee_tcp.pv` query 3	an agent never dials a target the relay names; a session without a fixed target is refused
`nfltr http --e2ee` raw TCP	its unpinned raw sessions still dialled the relay's target: a hostile relay could reach the agent's network	the audit after the finding above	raw sessions only with a fixed `--tcp-forward`
client auth	the agent asked for no client certificate, so the relay opened a pinned session of its own and reached the service	ProVerif, `e2ee_tcp.pv` query 7	client pins: the agent lists the client keys it serves, required for an end-to-end service
hub-remote refusal	deliver a forged row under the device's sender and the real row's command id; the page showed an approval the hub had accepted as refused	ProVerif, `hubremote.pv` query 6	the hub names a device only after the envelope verified; the page matches acks by its own signed message id
p2p nonce	AES-GCM nonce reuse: a write that failed partway gave its sequence number back, so the next frame was sealed under the same nonce	reading the code below the model (nonces are not symbolic)	a failed write spends its number and ends the connection. That fix covered the sealed signalling frames; the data path's records had the same gap, found by a later review of this post's claims and fixed after v2.1.54 (`TestSecureConnFailedWriteEndsIt`)
share label	an `nfltr http` share with no certificate of the agent's own printed "Verified ... Blind relay is active", and the dashboard showed a placeholder as its fingerprint, while the relay's own certificate ended its TLS	a review of this post's claims, checking the certificate the share's host served	a share without the agent's own certificate says it is relay-terminated, and no placeholder is shown as a fingerprint (`TestShareWithoutAgentCertificateIsRelayTerminated`)
finding 5 (WireGuard, P2P) name not bound	reroute a client to another exit or responder holding the same machine key	ProVerif, `wg_exit.pv` 4, `p2p_e2e.pv` 3	the exit's or responder's name in the preshared key and salt
S1 (A2A sessions, design)	forge "unknown" where the callee had run the call, or hold the resume back: the retry ran the request twice	TLC, before the code landed	the retry names the resume; the callee refuses it or takes its number
S2 (A2A sessions, high)	after a key rotation while a resumed call waited, forge "unknown": the caller retried under the new key and the call ran twice	the trace recorder: a run of the real code, checked against the TLA+ spec, was rejected	a call whose key no longer holds ends instead of retrying
K1 (A2A keys, high)	name a leaked machine's id to `nfltr node join` on the hub's machine: it derived that machine's key and dialled with it, so the relay read that node's calls	the code checked against `a2a_keytransfer.pv`: it was mutant `relay-names-id`	node join refuses an id the store already has
K2 (A2A keys, high)	list one machine's agent with a leaked machine's id in its machine label: the hub keyed its calls to that agent with the leaked key, and the relay read them	the code checked against `a2a_machine.pv`: it was mutant `no-target-check`	a label keys a call only when it is the machine the agent ref names
K3 (A2A keys)	resolve a name given to `nfltr orch hub machines add` to a leaked machine's id: its key was written again, for the owner to install on the machine they meant	the audit after K1	an issued id is written again only when the owner types it
K4 (WireGuard, P2P, high)	name another machine's key id (`x-wg-peer-key-id`, the key id in a p2p answer) to a client holding the root key file: it derived that machine's key, so the relay moved `lab.lan` to `lan` on another machine you added or, with a leaked machine key, sat in the middle	a review of this post's claims, then `wg_exit.pv` and `p2p_e2e.pv`: the code was mutant `relay-kid`	a root key holder takes only the machine it named: a ref's, or the one its own store holds under `<machine name>` (the name given to `machines add`); a bare service name, the root key
CL4 (A2A calls, low)	a caller that refused its own call at a revoked key still sent a cancel for it: harmless at the target, but a first frame after it would start a handler whose caller had left	the nightly trace check of the call lifecycle spec rejected the run	a cancel only once a frame of the call went; the invariant `CancelKnown` and its mutant guard it

The pattern: most of these are not broken cryptography. They are a check that was missing (which target, which client, which callee), a field that was not bound into a transcript, or a fallback a relay could steer to. A symbolic model finds exactly those, because it lets the attacker try every message it can build.

One attack, step by step

The relay-named target, as ProVerif found it in e2ee_tcp.pv:

The protocol before. The agent ran nfltr tcp --e2ee with no --forward, so nothing fixed what it served. A client opened a pinned session. The relay's open message named the target to dial, and the agent took it.
What the relay changes. It writes a target of its own choosing into the open: a host it controls, or one on the agent's network.
What the agent did wrong. The TLS handshake succeeds: the client sees the pinned key and the relay can't read the records. The agent then decrypts the client's bytes and writes them, in plaintext, to the target the relay named.
The trace. Query 3 (the payload of an end-to-end nfltr tcp without --forward stays secret) fails. The attack ProVerif prints has the attacker learn the payload by naming a target it reads from. The pin, the TLS and the client keys are all intact; the leak is one hop after the encryption ends.
The fix. An agent never dials a target the relay names. An end-to-end session without a fixed target is refused.
What holds now. Query 3 holds. The mutant that puts the old behaviour back ("the relay's target without --forward") must fail query 3 on every push, so a change that brings the bug back fails CI.

Evidence: the models and their results

Setup: ProVerif 2.05 and OCaml 4.14.2 built from source pinned by sha256; eight models of the E2EE paths in four repositories, plus wire v1's kept as the findings' evidence (relay: a2a_machine.pv, a2a_today.pv for wire v1, e2ee_tcp.pv, wg_exit.pv, p2p_e2e.pv; relay-core: e2ee_share.pv; the relay server and nfltr repositories: the WireGuard relay, hub remote and key transfer models).
Numbers: 75 runs per push (relay 55, relay-core 5, relay server 3, nfltr 12): each model's base line, its two-relay and leak variants and one line per mutant. Every base query of the current protocols holds, witnesses aside, except the documented limits (pinned TCP 5, 6; WireGuard unpaired 3; P2P unpaired 5; share links 2; hub remote 8, 9), and every mutant fails the queries it targets.
Reproduce: in a clone of github.com/nfltr/relay or relay-core, make spec-proverif; PROVERIF_OUT=<dir> keeps every log with its attack traces.
Limits: Symbolic models: perfect cryptography, no nonces, no timing; the code is tied to them by citations, wire vectors and tests, not by a verified implementation. Three of the eight models are in private repositories.

What is assumed

assumption	source
TLS 1.3 with a checked server key is an authenticated channel; no resumption skips the pin check	Cremers et al., IEEE S&P 2017; Bhargavan et al., IEEE S&P 2017; the agent's TLS configuration sets no session cache
Noise IKpsk2 (WireGuard) gives a key only to the holder of the peer key it used and the same psk	Donenfeld and Milner 2017; Dowling and Paterson, ACNS 2018; Lipp, Blanchet and Bhargavan, EuroS&P 2019
Noise NNpsk0 as specified	Noise Protocol Framework rev. 34
DTLS-SRTP keys only the holder of the fingerprinted certificate	RFC 5763, RFC 8827
X25519 refuses low-order points; SHA-256, HMAC, HKDF, AES-GCM are ideal, nonces unique per key	RFC 7748, Go `crypto/ecdh`; RFC 2104, RFC 5869; NIST SP 800-38D
a key file the owner copies (scp, a USB stick, a paste) is a channel the relay neither reads nor writes	the owner's choice of channel
a 0600 file is readable only by its owner	POSIX

What is not proven

First use. A pin, a fingerprint, an SSH host key or a key file is only as good as the way it reached the other end. Pinned TCP trusts the fingerprint you carried from the agent's own output; nfltr shell trusts OpenSSH's first-use prompt, and every start without --host-key is a new first use; WireGuard and P2P without a key file trust the relay on every connection; the hub's pairing trusts the page the relay serves at that moment. Never take a pin from a page the relay serves.
One known gap in A2A sessions (L1). A callee that restarts right after serving a resumed call, with the relay forging its "unknown" within the 5-minute retry bound, runs that call again: nothing survives a restart. It is stated in the spec and accepted for now.
Metadata and side channels. The relay sees who talks to whom, when and how much (TLS record sizes, packet sizes and timing). No model covers traffic analysis, or timing and cache side channels in the cryptographic code.
The implementation beyond the modelled rules. A symbolic model checks the protocol as modelled. The code is tied to it by file and line citations, wire vectors, one test per finding and a drift check; that is evidence, not a proof that the Go code implements the model. The p2p nonce finding was below the model, found by reading code.
Which machine a root key file reaches (WireGuard, P2P). A client or P2P caller holding the root key reaches only the machine it named: a ref's machine, the machine its own store holds under a name (the name given to nfltr orch hub machines add <name>, which the relay resolved once, at add), or the root key for a bare service name (K4). A machine added by its id or by nfltr node join has no name there: name its agents by ref. A P2P responder names no caller, so it takes a call from any machine in its store, a leaked one included until it is revoked. A machine key file reaches only agents under that one key.
Revocation timing. A removed client key is refused from the agent's next start; a session already running continues until it ends. A machine revoked on the hub's machine has its A2A calls end at once, but it still opens frames sealed before its revoke (harmless). A machine revoked in the account reaches the hub's A2A keys within 5 minutes, through the relay: a hostile relay can withhold it, so against such a relay revoke on the hub's machine. A relay can delay, though not forge, what it carries.
Denial of service. Every relay can refuse to carry anything; no model claims otherwise.

What it costs

ProVerif runs in each repository's make ci, on every push. ProVerif itself is built once from source per machine (a few minutes) and cached.

Evidence: ProVerif time per push on our Linux CI runner

Setup: The make spec-proverif step of make ci, on our Linux CI runner, on the six latest green pushes of the relay, relay-core and the relay server and the four latest of nfltr, 2026-11-08.
Numbers: relay: 284 to 322 s of ProVerif in each of the six pushes (598 to 667 s of CI each), 45 to 50 % of their CI time; the slowest line, the session model with the root key leaked, 223 to 247 s. relay-core under 1 s, the relay server under 1 s, nfltr 3 to 6 s.
Reproduce: make spec-proverif in a relay clone prints each line's seconds; make ci prints the step's.
Limits: One runner type, other jobs on the same machine; the time grew with the session model, which runs in every variant.

Almost all of it is one model: the A2A handshake with sessions, in each relay variant and against each mutant. The other models take seconds.

Rerun it

The models for the relay's own paths are public. With a C compiler, make and curl:

git clone https://github.com/nfltr/relay
cd relay
make spec-proverif

That builds ProVerif once into a cache and runs every line of spec/proverif/expect.txt: A2A wire v2 with sessions in every two-relay variant, wire v1 with its findings, pinned TCP, WireGuard and P2P, each with its mutants. spec/proverif/README.md explains every query, every mutant and every finding, and maps the models to the code. github.com/nfltr/relay-core holds the share-link model the same way. To see an attack, put a mutant's flag on a model (./spec/proverif/run.sh e2ee_tcp, then edit a line of expect.txt) and read the trace in PROVERIF_OUT.

The other models are in private repositories: the WireGuard relay's tenant isolation in the relay server, and the hub's paired devices and the machine key transfer in nfltr. They use the same runner, layout and pinned prover; their queries and results are listed above.

Is it for you?

Fits if you want a relay you do not have to trust with the content of your traffic: pinned TCP sessions with client pins, WireGuard and P2P with a pairing key, and agent-to-agent calls between your hub and your machines are proven against a relay that lies, alone or with others.

Not ready for hiding who talks to whom or how much, protection when the first key travels through the relay, or a formally verified implementation: the proofs are of the protocol as modelled, tied to the code by tests and citations.

Try next: pin an agent and list your client keys (TCP and SSH tunneling), give WireGuard and P2P a pairing key (pairing keys), or run make spec-proverif in a clone of the relay and break a model with one of its mutants. For the state machines behind the A2A sessions, see What TLA+ found in nfltr.