# NCP — Formal Verification Report (ProVerif, Rounds 3 and 5)

> **Public edition, published 30 October 2026**, with the NCP specification (draft 0.6). The models and the
> reproducible harness are in `ncp-proverif-models.zip`: unzip, then `docker build -t ncp-proverif . && ./run-all.sh` runs
> every query; `RESULTS.txt` is our run. Licence: CC BY 4.0 (this report), MIT (the models).


**Date:** 2026-07-11. **Target:** NCP draft 0.3 → **0.4** (the two new key-agreement paths added in
0.2 — §6.3 identity-hiding wrap, §11.4 session-reset). **Tool:** ProVerif (symbolic, Dolev-Yao).
Models + reproducible harness: the published ProVerif models (`ncp-proverif-models.zip`). 

> **Headline:** every targeted property **verified**, and the check **found one real
> authentication gap** in the draft-0.3 reset (one-way key confirmation → A not authenticated to B),
> now fixed by mandatory mutual key confirmation and re-verified. This is the Round-3 gate the spec
> required before P1 implementation.

---

## 1. Why ProVerif (and its limits)

ProVerif is the tool the Inria team used for the real-world PQXDH analysis; it proves reachability,
secrecy, and (injective) authentication in the symbolic Dolev-Yao model, with native support for the
Diffie-Hellman equation. It is the pragmatic choice to actually *run* here (one-line opam install in
Docker) versus Tamarin (Haskell/Maude toolchain).

**Symbolic-model caveats — what ProVerif does NOT capture (handled elsewhere, not gaps):**
- **Computational/encoding attacks** — e.g. the Round-2 X25519 top-bit malleability (finding #13) and
  ML-KEM's non-binding property. These live below the symbolic abstraction; they are addressed by the
  transcript/AAD binding fixes (§6.2/§6.3) and, crucially, by keeping the proof robust to a *total*
  KEM break (the hybrid result §4.4), so a KEM-binding failure cannot by itself break a session.
- **Deniability** — argued from the no-signatures design (§6.5); a full proof needs observational
  equivalence, out of scope for this pass.
- **The KEM is modelled as a correct, IND-CCA decapsulation function** (`decap(encap(pk,s),sk)=s`);
  the classical-break experiment (§4.4) is what ensures we never *rely* on KEM properties beyond that.

## 2. How the protocol was modelled

| NCP element | ProVerif model |
|---|---|
| X25519 | `dh/2` with the standard commuting equation `dh(dh(g,x),y)=dh(dh(g,y),x)` |
| ML-KEM-768 | `encap(pk,ss)` / `decap(ct,sk)`; fresh `ss` per encapsulation |
| HKDF (SK/WK/RK0/confirm) | one-way functions of ALL their inputs (random-oracle style) — so an attacker needs *every* input to compute the output (this is what makes the hybrid property testable) |
| ChaCha20-Poly1305 | `senc/sdec` with associated data |
| Verified tier | invitation over a **private** `oob` channel (authentic) + publics leaked to the attacker; reverse-scan QR2 over a private `qr` channel |
| Connected tier | everything over the attacker channel `c` (negative control) |
| The relay | the Dolev-Yao attacker on `c` |

Each model includes a **reachability (sanity) query** to prove the honest protocol actually completes,
so a "secure" result can't be an artefact of a stuck process.

## 3. Files (the published ProVerif models (`ncp-proverif-models.zip`))

| File | What it checks |
|---|---|
| `ncp-handshake.pv` | §6.2+§6.3 Verified tier: joiner-identity secrecy, session-key secrecy, injective auth |
| `ncp-handshake-connected.pv` | **negative control** — Connected tier MUST fail (finds the disclosed MITM) |
| `ncp-reset.pv` | §11.4 reset: mutual injective auth + new-root-key secrecy |
| `ncp-reset-kci.pv` | §11.4 KCI resistance (peer's own long-term key compromised) |
| `ncp-reset-fs.pv` | §11.4 forward secrecy (both long-term keys leak post-session) |
| `ncp-hyb-pq.pv` | hybrid: KEM secret handed to attacker → key still secret |
| `ncp-hyb-classical.pv` | hybrid: all X25519 exponents handed to attacker → key still secret |
| `Dockerfile`, `run-all.sh`, `RESULTS.txt` | reproducible harness + captured output |

Reproduce: `cd ncp-proverif-models && docker build -t ncp-proverif . && ./run-all.sh`.

## 4. Results (verbatim query outcomes — see `RESULTS.txt`)

### 4.1 §6.2 handshake + §6.3 wrap — Verified tier — ALL PASS
- `inj-event(InviterAccepted(ikj,t)) ==> inj-event(JoinerRan(ikj,t))` — **true** (injective auth).
- `not attacker(IK_J_pub)` — **true** (the relay never learns the joiner's identity key — the wrap works).
- `not attacker(EK_J_pub)` — **true**.
- `not attacker(RK0-probe)` — **true** (session-key secrecy).
- reachability — honest run completes.

### 4.2 §11.4 session-reset — mutual auth + secrecy — PASS (after the fix, §5)
- `inj-event(BAccepts(t)) ==> inj-event(AInit(t))` — **true** (B authenticates A; injective ⇒ anti-replay).
- `inj-event(ADone(t)) ==> inj-event(BRan(t))` — **true** (A authenticates B).
- `not attacker(RK0'-probe)` — **true**.
- reachability — honest reset completes.

### 4.3 §11.4 KCI resistance — PASS
With B's **own** long-term identity private key leaked to the attacker:
- `inj-event(BAccepts(t)) ==> inj-event(AInit(t))` — **true**: the attacker still cannot impersonate a
  third party (A) to B. (`ADone⟹BRan` is *false* here — expected: with B's key the attacker can
  impersonate B, which is B's own compromised direction, not the KCI property.)

### 4.4 §11.4 forward secrecy — PASS
With **both** long-term identity private keys leaked in a later phase (post-session):
- `not attacker_p1(RK0'-probe)` — **true**: the new root key stays secret, carried by the
  ephemeral×ephemeral term `RD3 = X25519(EK_A,EK_B)`.

### 4.5 PQ-hybrid — PASS ×2 (harvest-now-decrypt-later resistance)
- **KEM broken** (attacker given `ss_pq`): `not attacker(probe)` — **true** (classical X25519 leg carries).
- **Classical broken** (attacker given all X25519 exponents): `not attacker(probe)` — **true**
  (post-quantum ML-KEM leg carries).
- Together: the session key is secure as long as *either* primitive holds — the hybrid guarantee.

### 4.6 Negative control (Connected tier) — FAILS as intended
Invitation over the attacker channel, no authentic reverse-scan:
- joiner-identity secrecy — **false** (leaks); injective auth — **false**.
- This is the spec's *disclosed* Connected-tier MITM (closed only by the §5.5 SAS step, out of
  symbolic scope). It confirms the models find real attacks and the Verified/Connected boundary is real.

## 5. The real finding (draft 0.3 → 0.4)

**Gap:** draft-0.3 §11.4 specified a **one-way (A→B) key confirmation** only. ProVerif proved
`B⟹A` injective agreement but **refuted `A⟹B`**: A (the reinstalling device) was **not** authenticated
to B's identity. Concretely, an attacker who substitutes `reset_resp` (choosing its own `EK_B`/`kem_ct`)
makes A derive a root key shared with the *attacker* while A believes it re-established with B — a
B-to-A impersonation on the reinstall path.

**Fix (draft 0.4, §11.4 step 2/4):** a **mandatory B→A key confirmation** — B folds
`confirm_B = AEAD(confirm_key, "B", reset_transcript)` into `reset_resp`, and A MUST verify it before
completing. With mutual confirmation, ProVerif verifies **both-direction** injective agreement
(§4.2). This correction was missed by the Round-1/2 manual + LLM-adversarial passes and caught only by
the formal check — the case for machine-checking before implementation.

## 6. Bottom line

The two new key-agreement paths are **formally sound in the symbolic model** with the draft-0.4
mutual-confirmation fix: secrecy, injective mutual authentication, KCI resistance, forward secrecy,
and PQ-hybrid all verified; the Connected-tier limit is exactly the disclosed one. Cleared for **P1
implementation**. A Tamarin cross-check with an explicit MAL-BIND KEM equational theory is a
nice-to-have, not a P1 blocker.

---

# Round 5 (2026-09-18, draft 0.5): `pq_rekey` root-step rule and the lease race

**Why:** Round 4 (F1) found the v2-plan wording of `pq_rekey` circular and order-ambiguous; spec 0.5 §7.5
moved the KEM material into the DR-HE header and bound the KEM secret to the chain whose header carries
the ciphertext. §7.5 requires this rule to be machine-checked before the P1 feature flag is enabled.
Round 4 also asked for a model of two devices racing a §11.1a lease take-over.

**How modelled.** A simplified root chain: RK0 shared from the hybrid handshake; Alice starts a chain
with `hdr{g^a1, pq{e, pk_e}}`; Bob answers at his next chain start with `hdr{g^b1, pq{e, ct_e}}`; the
root step keyed by Bob's chain uses `KDF_RK_pq(rk1, g^(a1*b1), ss_e, e)`. Headers are AEAD-encrypted
under a key derived from RK0 (DR-HE), so the relay cannot substitute `pk`/`ct`. A quantum adversary is
modelled as learning every X25519 shared value of the session (phase 1); a state snapshot as learning
RK0 (phase 1); "passive after the snapshot" is what the phase construction enforces.

| File | Checks | Result |
|---|---|---|
| `ncp-pqrekey.pv` | A1 — agreement: Alice's `rk2` = Bob's `rk2` (the chain-bound root-step rule is well-defined under a reordering/dropping attacker); probe secrecy; honest run completes | **agreement true · secrecy true · reachable** |
| `ncp-pqrekey-heal.pv` | A2 — **post-quantum post-compromise healing**: attacker later holds RK0 (pre-epoch snapshot) + every DH shared value; `sk_e` was zeroized | **probe stays secret (true)** |
| `ncp-pqrekey-heal-classical.pv` | A3 — **negative control**: same leak, classical root step only (no KEM) | **probe LEAKS (attack found)** — A2's result is carried by ML-KEM, not by the model |
| `ncp-pqrekey-hyb-pq.pv` | A4 — hybrid: the epoch's KEM secret `ss_e` handed to the attacker outright | **probe stays secret (true)** — the classical leg carries |
| `ncp-pqrekey-snapshot-sk.pv` | A5 — the documented caveat: the snapshot also contained the pending `sk_e` | **probe LEAKS (as §7.5 states: healing at the *second* boundary; hence immediate `sk_e` zeroization)** |
| `ncp-lease-race.pv` | B1 — two devices with the same vaulted `otok` race `rotate_otok`, modelled as an atomic compare-and-swap (linear resource); **no fork**: a token the server accepts for a fetch is decoded by at most one device | **true** (sanity queries not reconstructable in this encoding — see B2) |
| `ncp-lease-race-reach.pv` | B2 — same race with an explicit if/else bounded server; honest completion | **rotate + winning fetch reachable for either device** (no-fork undecidable in this encoding: ProVerif abstracts inequalities) |

**Reading.** (1) The §7.5 rule is sound in the symbolic model: both sides derive the same root key
regardless of message order, and one KEM epoch restores secrecy against a quantum-capable adversary who
held the previous state — with the classical control proving the model can see the difference.
(2) The hybrid property holds for the rekey path as it did for the handshake. (3) A5 is not a finding
but a confirmation of the stated caveat. (4) The lease no-fork property holds **given** the server
implements `rotate_otok` as an atomic compare-and-swap on a single live owner token (the P2 invariant:
one-row conditional update, tested in Suite 78); ProVerif cannot decide mutable-state inequalities, so
the two encodings split the work — B1 proves, B2 witnesses. A Tamarin model (native mutable state) is
the tool if a single-model proof is wanted later; P1's property tests cover the schedules.

**Caveats (unchanged from Round 3):** symbolic model; KEM as ideal decapsulation (binding handled by the
`SHA-256(pk||ct)` in the KDF info, §7.5); no side channels; no modelling of `MAX_SKIP` or the skipped-key
cache. **Not modelled:** more than one epoch (the rule is per-epoch and identical), header padding.

**Consequence:** the `NCP_PQ_REKEY` feature flag may be enabled in P1 once the implementation's fixtures
match the reference; the human design review (G0) remains the gate for publishing the security claims.

Reproduce: `cd ncp-proverif-models && ./run-all.sh` (14 models; `RESULTS.txt` is the captured output).