The Nygma Chat protocol, in the open.

Draft 0.5.3 changelog (2026-10-16, product decision; design record internal design record): one new carrier form and UI rules — no change to keys, KDFs, the handshake, the ratchet, envelopes, the attachment format or the server protocol. §5.3b (new) — the in-person QR carries the claim code (ncp:i# ‖ base64url(s) ‖ . ‖ code): the scanning phone sends it with its first fetch, so pairing in person has no code step. This changes S1 ("the code never travels with the invitation") for that QR only — a photo of it lets someone else join while it is valid — with normative mitigations: single use, at most 10 minutes, revoked when the inviter's screen closes, a "show only to the person in front of you" warning, and "Someone joined as …" with "Not them? Remove this chat". Links are unchanged: no link form can carry a code; §5.3's sequencing and 3-strike burn stand. §4 / §5.2 / §5.3a / §5.4 — verification is optional: no verify step in either flow (QR₂ is no longer shown after joining), no verify nudge or "Connected" label in the chat; Verified (green badge) is reached through Chat info → Verify security (§5.5 SAS and the §5.2 QR₂ check, unchanged). §4 / §11.4 — key change: after an unattended reset the peer shows ONE quiet system line ("<name>'s security code changed (new phone or reinstall)") instead of the Check-again banner and blocked composer; a Verified channel returns to Connected and its line says so. §10: the attachment limit is the sender's plan's largest file (100 MB … 2 GB, applied by the app); presigned chunk URLs are re-requested during long transfers.

Draft 0.6 changelog (2026-10-20, product decision — message actions): additive inside the ratchet AEAD, no key schedule, envelope or crypto change; existing golden vectors byte-identical, seven appended. §8 every content payload carries a sender-chosen mid (16 random bytes, the one message identity both phones share) and may carry re (a reply: target mid + o, never a copy of the target's content); new types react, edit, del; control kinds protect, screenshot; receipts name mids (m), seqs kept for 0.5 peers; the ign forward-compatibility rule; optional extension fields decode leniently. §8b the receiver's rules (edit = author's own text ≤ 15 min, delete for everyone = author's own messages ≤ 48 h with no trace, reactions one per person; windows on the author's clock + an arrival bound). §9.2 x-ncp-quiet (no push poke for receipts / edit / delete) and the sender's early blob delete (DELETE blob/{id} with a delete token, §10.5). §11.2 blind mid index; one durable FIFO send queue per channel on the client. §11.3a "Protect this chat" (per-person flag, strictest wins, both phones) and the screenshot notice. §11.3's "block screenshots by default" line corrected to the 2026-10-16 decision.

Draft 0.5.2 changelog (2026-10-10, product decision): additive, no crypto change. §9.2 recv returns, outside the ciphertext, a coarse server receive time at per envelope and the server clock now; the receiver shows a message at that arrival time on its own clock (WhatsApp-like) instead of the sender's payload ts (sender-clock skew showed messages hours in the past). Payload ts is unchanged.

Draft 0.5.1 changelog (chat feature round, 2026-09-23): additive, no key schedule or envelope change. §8 payload catalogue gains location (static, signed micro-degrees, §8a) and the forward-compatibility rule (a strict codec still rejects unknown t/kind; the client renders a placeholder and advances the ratchet instead of dropping the message). §10.3 media pointer gains optional dur (seconds, voice notes). §12.14 documents the client-side, off-by-default map preview and exactly what it leaks. Multi-item sends are N ordinary media messages grouped on display only — no album payload (product decision).

Draft 0.5 changelog (Round-4 independent review, 2026-09-18; see §16 and internal review notes): the July core (§6, §7.1–§7.3, §11.4 reset) is unchanged. Changes: §7.5 pq_rekey (new, v1): periodic ML-KEM-768 re-injection carried in the encrypted DR-HE header on every message of a chain, mixed into the root step keyed by that chain's dh_pub; fixed header size HDR_CAP (§7.2, §8). §5.3 claim code (peppered HMAC gate, 3-strike BURNED, possession poll_tok, OPENED = blob fetched) and the corrected "detectable by the joiner, not the inviter" wording; commitment-QR form not adopted (bootstrap deadlock), form field added; link hosts nygma.genie9.com. §9.2 rotate_otok, client-chosen queue label echoed in pokes, quota as per-account create-rate (blind tokens v1.x), no separate relay service. §11 rewritten for the two-key model: K_wrap/K_work/K_store layering (hardware-wrapped, not credential-gated — the PIN gate is app-enforced), PIN-first Chats gate reusing the existing duress PIN slot, session-wide duress state, decoy Chats = first-run state, content-free notification default, fixed-slot padded working store, §11.1a lease (record_version, approved vs unattended take-over, control:superseded, loud alert), fixed-size ncp-channels container per drive, strong mode per drive. §12 honest P9 rewrite, §12.9 PQ claim corrected (HNDL already defeated for the session; pq_rekey = PQ post-compromise healing), §12.6 deniability (content yes, participation no), new items 13–16. §14 corrected (JS ML-KEM; expo-crypto; SQLite; camera; App Links).

Draft 0.4 changelog (Round-3 formal verification; see §16): the two new key-agreement paths were machine-checked in ProVerif (Dolev-Yao model). The Verified handshake+wrap and the reset's anti-replay, KCI-resistance, forward-secrecy, and PQ-hybrid properties all verified. The check found one real gap: the draft-0.3 reset had only a one-way (A→B) key confirmation, so A was not authenticated to B (an attacker substituting reset_resp could impersonate B to a reinstalling device). Fixed by adding a mandatory B→A key confirmation (confirm_B folded into reset_resp) — mutual key confirmation, re-verified in ProVerif (both-direction injective agreement now holds). Models committed under the published ProVerif models (ncp-proverif-models.zip); report the formal verification report (published with this spec).

Draft 0.3 changelog (Round-2 review; see §16 for the full finding→fix log): the §6.3 identity-hiding wrap is confirmed sound; applied its mechanical fixes — wk_j removed from the §6.2 transcript (a relay could otherwise flip its top bit to silently desync SK and burn the single-use invitation), kem_ct now bound into the wrap-key info (ML-KEM non-binding hardening), ss_pq zeroization made explicit, and the q_reply.srv allowlist check generalized to every written queue. The §11.4 session-reset was REDESIGNED — the draft-0.2 one-sided static-authenticated message had no forward secrecy, no anti-replay, no KCI resistance, and dropped the PQ leg; it is now a two-message, mutually-ephemeral, hybrid-PQ, epoch-bound, key-confirmed re-handshake with its own transcript + domain labels. SAS reconciled everywhere to 8 words / 2⁸⁸. Added disclosures (persistent-qid cross-reinstall device linkage; reinstall reset-burst vs duress) and a re-vault invariant for rotated write tokens. Two RN production landmines flagged normative: a CSPRNG health-check gate and native (not pure-JS) ML-KEM decapsulation.

Draft 0.2 (superseded): fixed a fatal Double-Ratchet init contradiction (C1); joiner sends first; inviter retains its ephemeral to the first ratchet step; JoinMsg wrap added; DR-HE header keys + length-hiding padding pinned; P7/P8/P9 claims reworded with real mitigations.

---

1. Goals and security properties

NCP establishes and operates a channel: a long-lived, 1:1, end-to-end-encrypted messaging relationship between two devices, bootstrapped exclusively out-of-band (no server key directory exists), delivered through an untrusted store-and-forward mailbox server.

Targeted properties (with honest scope — see §12):

Non-goals (v1): group messaging (v2 = MLS); multi-device identity (each device pairs independently); voice/video; anonymity against a global network observer; protecting a compromised endpoint.

2. Cryptographic primitives

Hybrid rule (normative): every session secret MUST mix X25519 output(s) and the ML-KEM shared secret through HKDF, so the session is secure if either algorithm holds. Classical security MUST NOT depend on ML-KEM correctness (relevant while @noble/post-quantum awaits an independent audit).

At-rest storage of channel/message artifacts inside a drive reuses the existing ZK-v2 artifact scheme (nygma-crypto.contract.ts: subkey = HKDF(baseKey, ∅, "type:fileId"), fresh IV, AAD v2:fileId:type) with the drive's configured algorithm — see §11.

Encoding: canonical CBOR (RFC 8949 §4.2 deterministic encoding). URL-carried binary is base64url without padding. Multi-byte integers big-endian. Transcript hashes are computed over received/transmitted octet strings, never over a re-serialization (§6.2).

3. Entities and roles

• Inviter (I) — creates the channel and the invitation. Plays the Bob role in the ratchet.
• Joiner (J) — consumes the invitation, drives the handshake, and sends the first ratchet message. Plays the Alice role.
• Mailbox server (S) — untrusted store-and-forward (§9); assumed able to read/modify/drop/replay anything it stores and to be compelled. All guarantees except availability MUST hold against a fully malicious S.
• Channel — the pairwise relationship; channel_id = 16 B random, client-side only.

3.1 Identity model — pairwise, per-channel

Each device generates a fresh identity keypair per channel: IK (X25519). No global chat identity, username, or directory entry. Normative:

• IK_priv MUST be generated at channel creation/join, MUST NOT be reused across channels, and IS persisted (vaulted, §11.1) so the channel can be re-established after reinstall (§11.4).
• No key is ever placed in, or served from, a server-side directory. The relay does handle the ciphertext envelopes it forwards; the joiner's identity key IK_J is wrapped so the relay never sees it in cleartext (§6.3). The invitation ephemerals that appear on the wire are single-use and unlinkable to any account or directory. (This is the precise, honest form of the earlier "server never sees a key" claim — see §16/H2.)

4. Trust tiers

0.5.3 (product decision 2026-10-16) — key change without a banner. After an unattended §11.4 reset the peer adds ONE quiet system line to the thread — "<name>'s security code changed (new phone or reinstall)." — and keeps the composer enabled. A Verified channel returns to Connected and its line adds "This chat is no longer verified." The old session's SAS material is discarded (it describes keys that no longer exist). An approved take-over (control:superseded, §11.1a) stays silent, as before.

There is no tier in which a key is accepted from the server.

5. Bootstrap

5.1 Invitation payload

Invitation = CBOR {
  v:      1,
  form:   uint,           ; 1 = full (QR/link carries the whole Invitation), 2 = short-link blob (§5.3)
  inv_id: bytes(16),
  ik:     bytes(32),      ; IK_I public (X25519) — channel identity, fresh per §3.1
  ek:     bytes(32),      ; EK_I public (X25519) — ephemeral, single-invitation, doubles as I's
                          ;   initial ratchet key (retained until first ratchet step; see §6.4/§7.1)
  kem:    bytes(1184),    ; ML-KEM-768 encapsulation key, fresh per invitation
  q_join: QueueRef,       ; J→I queue: { srv, qid:bytes(16), wtok:bytes(32) }
  exp:    uint,           ; unix seconds; MUST be ≤ 48h from creation
  ? at:   bytes(8),       ; OPTIONAL same-account tag (2026-09-20, an earlier issue): HMAC-SHA256(K_meta[chats drive],
                          ;   "ncp1/same-account")[0:8]. Opaque to everyone but the inviter's own account;
                          ;   a joiner whose own tag matches MUST refuse ("invitation from your own account").
}
QueueRef.srv MUST be one of the client's built-in allowlisted server origins (§9.1) — an
invitation MUST NOT be able to point a client at an arbitrary URL.

• EK_I and the ML-KEM keypair are freshly generated per invitation. IK_I is the channel identity (fresh per §3.1). The inviter pre-creates q_join (§9.2).
• Single-use: the inviter MUST accept at most one join per inv_id.
• inv_octets (§6.2) is the exact octet string the joiner received in the form used: the decoded Invitation bytes for form 1, the decrypted blob plaintext for form 2. Both sides hash the same octets.
• A "commitment QR" form (QR carries H(kem), KEM key fetched later) was considered in v2 of the plan and rejected (Round-4 F2): the joiner cannot build JoinMsg without kem, and the inviter has no path to the joiner before JoinMsg — a bootstrap deadlock. The full-Invitation QR (form 1) is the offline form: ncp:i# ‖ base64url(Invitation) ≈ 1.8 K chars → QR version 31 at ECC L. S0 scan test (2026-09-18, POCO X3 Pro, expo-camera): a 1806-char form-1 QR scanned from a laptop screen on the first attempt with an exact hash match (internal engineering notes §4). Form 2 (short link) stays the default because it also scans from a phone screen at arm's length.

5.2 Verified ceremony — mutual QR scan (in person)

1. I displays QR₁. Default: the short-link form ncp:i# ‖ base64url(s) (≈60 chars; the AEAD blob is fetched from S per §5.3 — S cannot read, forge or substitute it, it can only deny; both phones need connectivity during the ceremony). Offline form 1: ncp:i# ‖ base64url(Invitation) (self-contained; QR version 31; verified scannable in S0 — see §5.1) — offered as "No connection? Show the offline QR". Either phone may scan first: a "Scan their code" entry exists beside "Show my QR", and a phone that has just been scanned advances to its own camera step.
2. J scans, runs the handshake (§6), posts JoinMsg + its first ratchet message (completes in seconds while co-located).
3. J displays QR₂ = ncp:c# ‖ base64url(CBOR{ inv_id, fp: transcript }) (§6.2 transcript).
4. I scans QR₂ and MUST verify fp == its own transcript. Match → both mark Verified; I signals J via an authenticated control:verified on the now-established (transcript-bound) channel so J also transitions. Mismatch → I MUST abort and destroy the channel.

Machine-checked in both directions; no human string comparison (research: humans fail at it). The client MUST show distinct terminal screens for success ("both phones agree") and mismatch ("no chat was created").

0.5.3: pairing in person no longer runs this ceremony as part of joining. The inviter shows the §5.3b QR (the short form WITH the claim code); the joiner joins and opens the chat — QR₂ is not shown. Steps 3–4 (QR₂ and its machine check) and §5.5 stay available, optionally, from Chat info → Verify security, and are what makes a channel Verified.

5.3 Connected ceremony — one-time link (remote) with claim code

Hosts: https://nygma.genie9.com/ch#… in production development. Both hosts serve /ch App Links (Android assetlinks.json, iOS AASA) and a landing page for phones without the app (§5.3a). The payload is always in the URL fragment (never sent to any web server).

Full link (form 1): …/ch# ‖ base64url(Invitation). Short link (form 2, default):

1. I: s ← random(32); blob_id = HKDF(s, ∅, "ncp1/invblob/id", 16), blob_key = HKDF(s, ∅, "ncp1/invblob/key", 32), poll_tok = HKDF(s, ∅, "ncp1/invblob/poll", 32), nonce = random(12).
2. blob = nonce ‖ ChaCha20P.Enc(blob_key, nonce, CBOR(Invitation), aad="ncp1/invblob"‖blob_id).
3. Claim code (default on, product decision 2026-09-18): I draws code = 6 random decimal digits, shown to the user in Latin digits regardless of locale, never placed in the link (0.5.3: in no link form; the in-person QR of §5.3b is the only carrier that holds it), and computes H = HMAC-SHA-256(pepper, "ncp1/claim" ‖ blob_id ‖ code) where pepper is a server-side secret held outside the database (the server itself computes H; I sends code to S over TLS at upload — the code is not a secret from S, see the security notes). Without a claim code, H = ∅.
4. I uploads (blob_id, blob, exp, H?, poll_tok_hash = SHA-256(poll_tok)) under an upload grant against I's quota (§9.2). S stores it one-time. Expiry is server-authoritative.
5. Short link = …/ch# ‖ base64url(s) (≈ 60 chars).
6. J opens the link → derives blob_id, blob_key → if the server reports a claim code is required, the app asks for the 6 digits → fetch(blob_id, code?). S checks H; a mismatch increments a server-side attempt counter; on the third mismatch the blob transitions to BURNED (distinct from CLAIMED, NOT_FOUND, EXPIRED, REVOKED). A correct code (or no code required) atomically marks the blob CLAIMED and returns it; later fetches return CLAIMED.
7. J atomically persists s + the fetched Invitation locally before any further step (crash-safe, §5.4) → proceeds to §6.
8. I polls invitation state with poll_tok (possession, never the account session — an account-authenticated poll would bind account → blob_id → q_join and defeat the account-less send path).

UI sequencing (normative for clients): the link is shown and shared first; the code is revealed only after the share sheet returns, naming the app used ("You sent the link with WhatsApp. Now tell Nour the code any other way"). No copy affordance on the code by default. Otherwise both artefacts travel in one thread and the code protects nothing.

Security notes (normative consequences):

• S never sees s/blob_key → it cannot read, forge, or substitute the invitation (AEAD under a key it lacks). It can only delete/deny (availability).
• The claim code is not a secret from the server; the server is a rate limiter. It protects against everyone who is not the server: a link interceptor or a blob-at-rest thief now also needs the channel that carried the code. A link-only attacker succeeds with probability 3/10⁶. Say "the link alone isn't enough to join", never "cannot join". Mixing the code into blob_key would buy nothing (10⁶ offline trials against an AEAD tag are trivial); an OPRF/PAKE-gated fetch that makes the code a cryptographic gate against non-servers is reserved (§15).
• Interception is detectable by the joiner, not the inviter. If an attacker fetches first, the real joiner sees CLAIMED ("someone else may have opened it — tell the inviter"); the inviter sees a successful join and cannot tell. If the real joiner fetched first, the attacker learns nothing. The inviter-side signal that exists is BURNED (three wrong codes), which the inviter's client MUST surface in the chat list and the invite screen ("Someone tried the wrong code three times. Link destroyed."). A joiner that already claimed on this device MUST recognise its own persisted s and resume; the UI MUST distinguish "already opened here" from "CLAIMED by someone else."
• WRONG_CODE and CLAIMED are distinct responses, so a link holder learns whether the real joiner has already joined. Accepted and disclosed.
• Residual risk (honest): an attacker controlling the carrying channel who replaces the link (and, with the code on, also the code) before the joiner opens it achieves full MITM until SAS (§5.5, §12.2). Stated in the published threat model.

5.3a The invitee's path (informative, normative where marked)

1. Landing page, app not installed: names the inviter's self-declared name, says "install, then tap the link again", and MUST NOT fetch the blob (a page load never flips the invitation to OPENED). The fragment does not survive a store install on iOS; Android MAY carry it via the Play install referrer.
2. Landing page, app installed: opens the app with the fragment.
3. Account: email + one-time code, returning to the invitation.
4. Onboarding (product decision 2026-09-18): set the Nygma PIN → display name → done. A "Chats" drive is created with a device-generated random password (ordinary KDF v3 / key-wrap v2 flow — a random 256-bit string is a valid password), held under K_work (§11.2). Documented as weaker until the user sets a real password + recovery key from Security Hub or at first vault use (re-wrap, v2 format, own IV). Losing the device before that loses the chat identity and any vaulted history.
5. Code entry with attempts remaining; one distinct terminal screen each for WRONG_CODE, BURNED, EXPIRED, CLAIMED-by-other, REVOKED, offline.
6. First message: a persistent notice that the name is the inviter's own claim, a local nickname field, and one dismissible verify nudge per Connected channel. 0.5.3: no notice and no nudge in the chat; the nickname and the optional Verify security live in Chat info. The inviter's "Not them? Remove this chat" (§5.4) is the at-join check on the name.

5.3b In-person QR with the claim code (0.5.3, product decision 2026-10-16)

For two people side by side the inviter shows ONE QR; the joiner's app needs no code step.

1. Carrier: ncp:i# ‖ base64url(s) ‖ . ‖ code — the §5.3 short-form secret (exactly 43 base64url characters) followed by the 6 Latin digits of the same invitation's claim code (56 characters: QR version 4 at ECC M). Same invitation, same blob, same server flow as §5.3; nothing new is stored.
2. Parsing (normative): a claim code is accepted ONLY in this ncp:i# form. The https://<host>/ch# pattern, the bare payload and the app's own scheme MUST NOT carry or accept one, so a link can never carry the code. A form-1 (full) QR never takes a code. Older clients reject the suffix ("not a Nygma invitation").
3. Joiner: sends the carried code with its first fetch (§5.3 step 6); CLAIMED, EXPIRED, REVOKED and the attempt counter behave exactly as for a link. A code the user types (after WRONG_CODE) replaces the carried one. The scanned text is not echoed into an editable field.
4. Inviter (mitigations for S1, normative): the invitation is created with an expiry of at most 10 minutes (server-authoritative; the server accepts 1 s–48 h), is valid only while the QR's screen is open — closing the screen, switching to a link, or the Chats gate locking revokes it (DELETE …/invitation/{blob_id} with poll_tok; a locked client that cannot read its store still revokes at the server and drops the local row on the next open) — and never waits in the Chats list. The screen says "Show this only to the person in front of you." The code is never displayed on this path. After the join the inviter sees "Someone joined as '<their name>'" with "Not them? Remove this chat" (block-and-delete, silent to the peer).
5. What changes (S1): the code now travels with this invitation — anyone who photographs the QR while it is valid can join instead (and the real joiner then sees CLAIMED). Accepted by the product team for the in-person case only; the link path keeps S1. The full (form 1) QR stays available as a fallback behind "Other options", with a photo warning and the same 10-minute limit.
6. The QR text is not a web URL: a phone camera shows it as text and never opens the /ch landing page.

5.4 Invitation lifecycle

CREATED → OPENED → CLAIMED → COMPLETED | BURNED | EXPIRED | REVOKED. OPENED = the blob was requested (with or without a correct code); CLAIMED = the blob was returned. On COMPLETED the q_join queue persists as the channel's J→I infrastructure (its write token is rotated per §9 first). The inviter app MUST surface transitions in the chat list row and the invite screen: "Link not opened yet" / "Link opened · waiting for the code" / "Someone joined as '<their name>'" (with "verify it's them before sharing anything sensitive"; 0.5.3: with "Not them? Remove this chat" instead) / "Link destroyed after three wrong codes" / "Expired" / "Revoked". 0.5.3: a waiting link invitation's Chats-list row shows neither the code nor a copy action; it reopens the invite screen at its step. The inviter MUST NOT display "opened by <name>" — it cannot know who opened it. A CLAIMED not followed by a valid JoinMsg within 10 min SHOULD be surfaced as a possible interception — unless the same device reports it claimed the link itself, which is a benign crash-resume. Expired, burned and revoked invitations MUST have their q_join queue and ML-KEM/EK state garbage-collected (quota hygiene, §9.2).

5.5 SAS verification (Connected/Re-verify → Verified)

• sas = HKDF(sas_seed, ∅, "ncp1/sas" ‖ transcript, 11) → 88 bits → 8 BIP39 words (11 bits each; list already shipped) or emoji. sas_seed is a dedicated slice of the handshake output (§6.2), not the root key.
• Humans compare over a channel where they recognize each other (a call, or in person). Verification is mutual: each side confirms in-app; the channel becomes Verified only when both confirmations have been exchanged (control:verified in each direction); the UI shows "waiting for <peer> to confirm" in between; a "they don't match" on either side puts both channels into the Check-again state. Clients MUST render each word as a tile that must be tapped before the confirm action enables, and MUST NOT offer partial confirmation.
• The word list is language-independent: the same list rendered identically on both phones irrespective of device locale (English BIP39 words, with a numeric fallback "compare these 8 numbers" rendered in Latin digits). Localised word lists would make the ceremony fail between phones in different languages.
• Security-critical invariant: the SAS's MITM resistance depends on single-use invitations (§5.1). Because the victim's SK is frozen once it joins (single response), a dual-session MITM faces a second-preimage grind — ~2⁸⁸ work to make its separately-negotiated session hit the victim's fixed SAS — not a 2⁴⁴ birthday, which would require two grindable sides. Single-use invitations are what deny the second grindable side, so implementations MUST enforce them. (88 bits is chosen over a bare 66 to keep a comfortable margin above the "operational bound" a reviewer can question; an interactive commit-then-reveal round — the alternative hardening — is deliberately not used because it would break the asynchronous one-shot invitation model that is core to the product.) Partial comparison is a break, not graceful degradation: comparing k of 8 words leaves 11·(8−k) bits (e.g. 3 words → 2³³, offline-grindable). The UI MUST require all eight and MUST NOT present partial confirmation as "good enough."

6. Handshake — hybrid, OOB-authenticated, identity-hiding

6.1 Joiner key material

J generates fresh IK_J, EK_J (X25519) and a throwaway wrapping ephemeral WK_J (X25519), and computes (kem_ct, ss_pq) = ML-KEM-768.Encaps(kem). All received public keys are validated (§2).

6.2 Shared secret and transcript

DH1 = X25519(IK_J_priv, EK_I_pub)     ; authenticates J to I
DH2 = X25519(EK_J_priv, IK_I_pub)     ; authenticates I to J
DH3 = X25519(EK_J_priv, EK_I_pub)     ; ephemeral freshness

transcript = SHA-256( "ncp1/hs" ‖ inv_octets ‖ ik_j ‖ ek_j ‖ kem_ct )
             ; each term is the exact transmitted/received octet string (no CBOR re-encode)
             ; NOTE (Round-2 fix): wk_j is NOT in the transcript. It is a throwaway wrapping
             ; ephemeral that authenticates nothing about the session (peer auth rests on DH1–DH3 +
             ; ik_j/ek_j/kem_ct). Including it let a relay flip its RFC-7748-masked top bit — same
             ; decoded point (→ same WK, ct still decrypts) but different octets (→ different
             ; transcript) — silently desyncing SK and burning the single-use invitation. Out it goes.

SK = HKDF( ikm  = 0xFF×32 ‖ DH1 ‖ DH2 ‖ DH3 ‖ ss_pq,
           salt = ∅,
           info = "ncp1/hs/sk" ‖ transcript,
           len  = 96 )
   = RK₀(32) ‖ session_id(32) ‖ sas_seed(32)

• DH triple = X3DH mutual-identity binding; the one-time-prekey DH4 is unnecessary because EK_I is already single-use per invitation. Binding both the KEM key (inside inv_octets) and kem_ct into transcript closes KEM re-encapsulation/substitution (per the PQXDH analysis).
• ss_pq in the IKM makes the agreement hybrid (P5). 0xFF×32 is the X3DH domain prefix.
• session_id is the channel-binding AAD context; sas_seed feeds only §5.5. session_id is reconstructed locally by both parties and MUST NOT be transmitted anywhere (it shares an HKDF output stream with RK₀; keeping it off the wire keeps that stream's secrecy irrelevant to transport).

6.3 Join message (identity-hiding wrapper)

The relay must not learn IK_J. The joiner wraps identity/ephemeral fields under a key derived from material S lacks:

WK = HKDF( ikm  = X25519(WK_J_priv, EK_I_pub) ‖ ss_pq,
           salt = ∅,
           info = "ncp1/jmwrap" ‖ inv_id ‖ SHA-256(kem_ct ‖ kem),   ; kem = the invitation KEM pubkey
           len  = 32 )

JoinMsg = CBOR {
  v: 1, inv_id,
  wk_j:   bytes(32),     ; WK_J public — throwaway, unlinkable random point (cleartext)
  kem_ct: bytes(1088),   ; cleartext (random-looking); inviter needs it to Decaps
  ct:     bytes          ; nonce(12) ‖ ChaCha20P.Enc(WK, nonce,
                         ;   CBOR{ ik_j, ek_j, profile:{name?,avatar_ref?}, q_reply:QueueRef, pad },
                         ;   aad = "ncp1/jm" ‖ inv_id ‖ wk_j )   ; wk_j in the AAD → tamper = recoverable AEAD drop
}

Posted to q_join (invitation wtok) in a join-type envelope (§8). The relay sees only two random-looking points, a KEM ciphertext, and AEAD ciphertext — never IK_J. q_reply (the I→J queue) is pre-created by J.

• kem_ct + KEM pubkey are folded into the WK info (Round-2 hardening): ML-KEM is IND-CCA2 but not binding (neither MAL-BIND-K-CT nor -K-PK), so a KEM substitution could otherwise steer the wrap key. This mirrors the §6.2 transcript's KEM binding on the one new path that omitted it.
• wk_j is bound into the ct AAD so any malleation of the cleartext wk_j becomes a recoverable AEAD failure (retryable), never a consumed/burned invitation.
• Forward secrecy of the wrap: the joiner MUST zeroize WK_J_priv and the ML-KEM Encaps randomness/ss_pq immediately after posting JoinMsg. On the inviter side, because EK_I_priv is retained until the first ratchet step (§6.4/§7.1), ss_pq is the sole forward-secrecy-bearing half of the WK ikm during that window — so it MUST be zeroized at SK-derivation time (§6.4 step 4).

6.4 Inviter processing & first-message ordering (C1 fix)

On a join envelope, the inviter:

1. Verifies inv_id is CREATED/CLAIMED and unexpired (server-authoritative expiry + a skew grace margin); duplicate/second distinct JoinMsg for an inv_id → ignore (anti-replay).
2. Decaps(kem_ct) → ss_pq; WK = HKDF(X25519(EK_I_priv, wk_j) ‖ ss_pq, ∅, "ncp1/jmwrap"‖inv_id‖SHA-256(kem_ct‖kem), 32); decrypt ct (AAD "ncp1/jm"‖inv_id‖wk_j) → ik_j, ek_j, q_reply, profile. AEAD failure ⇒ drop silently, keep waiting. Then validate q_reply.srv against the built-in origin allowlist (§5.1) BEFORE any write or state commit — on failure, abort (do not mark COMPLETED, do not post). (Round-2: the round-1 srv-allowlist covered only the invitation's q_join; it now applies to every QueueRef a client writes to.)
3. Compute DH1–DH3 (with its private keys) → SK → transcript.
4. Initialize the ratchet in the Bob role, retaining EK_I_priv as the initial DHRs private key (§7.1). Destroy at this point the ML-KEM private key, the transient ss_pq value (Round-2: needed for wrap forward secrecy — see §6.3), and the invitation replay state — not EK_I_priv.
5. Rotate the q_join write token (§9) and mark inv_id COMPLETED.

The joiner sends the first ratchet message (§7): immediately after posting JoinMsg it posts a control:established (or the user's first text) to q_join. That message carries the joiner's new DHRs_J_pub; when the inviter processes it, the DH ratchet step consumes EK_I_priv (now safe to destroy), yields the inviter's receiving chain, and only then gives the inviter a sending chain. The inviter's chan_ack (carrying the rotated q_join write token and confirming establishment) is Bob's response, posted to q_reply — never the opener.

Lost-message rules (deadlock fix): the joiner MUST persist and retransmit the byte-identical JoinMsg and first ratchet message until it receives chan_ack; the inviter MUST re-send chan_ack on receiving an already-processed identical JoinMsg (dedup suppresses only distinct JoinMsgs, never the ack). A joiner handshake timeout surfaces explicit failure UX.

6.5 Authentication & deniability

• J→I: only the holder of IK_I/EK_I/kem (delivered OOB) can derive SK; a relay or link-observer cannot decrypt ct or complete the channel.
• I→J: SK depends on IK_J via DH1, so a valid chan_ack proves the responder controls EK_I_priv/kem and processed IK_J. Verified adds the QR₂ reverse transcript check; Connected's honest limit is "whoever holds the link," until SAS.
• No signatures anywhere → offline deniability (P6); the hybrid KEM does not break it (KEM possession is symmetric-simulatable given the transcript).

7. Message protocol — Double Ratchet with header encryption

Signal Double Ratchet + header encryption (DR spec §5.2), instantiated below. Joiner = Alice role, Inviter = Bob role (§3, §6.4).

7.1 Initialization (H5 / C1 fix — exact DR-HE assignment)

Two shared header keys are derived crosswise from the root: hka ‖ nhkb = HKDF(RK₀, ∅, "ncp1/hk0" ‖ session_id, 64) (2×32).

• Joiner (Alice): DHRs = generate (a fresh X25519 keypair that MUST differ from EK_J, so the first ratchet dh_out can never equal the handshake's DH3); DHRr = ek (I's invitation ephemeral EK_I_pub); (RK, CKs, NHKs) = KDF_RK(RK₀, X25519(DHRs_priv, DHRr)); CKr = None; HKs = hka; HKr = None; NHKr = nhkb. The joiner therefore has a sending chain immediately and sends first (§6.4).
• Inviter (Bob): DHRs = (EK_I_priv, EK_I_pub) (retained per §6.4); RK = RK₀; CKs = CKr = HKs = HKr = None; NHKs = nhkb; NHKr = hka. Bob gains CKr (and then CKs) only after processing the joiner's first message — which performs X25519(EK_I_priv, DHRs_J_pub) and consumes EK_I_priv.

The crosswise assignment (HKs_Alice = NHKr_Bob = hka; NHKs_Bob = NHKr_Alice = nhkb) lets each side trial-decrypt the other's first header.

7.2 KDFs (exact)

KDF_RK(rk, dh_out): HKDF(ikm=dh_out, salt=rk, info="ncp1/rk", 96) → rk'(32) ‖ ck(32) ‖ nhk(32)
KDF_RK_pq(rk, dh_out, ss_e, e, pk_e, ct_e):                        ; §7.5 — root step that consumes a KEM epoch
                    HKDF(ikm=dh_out ‖ ss_e, salt=rk,
                         info="ncp1/pqrk" ‖ LE32(e) ‖ SHA-256(pk_e ‖ ct_e), 96) → rk' ‖ ck ‖ nhk
KDF_CK(ck):         ck' = HMAC(ck, 0x02);  mk = HMAC(ck, 0x01)
Msg key expand:     HKDF(mk, ∅, "ncp1/mk"‖session_id, 44) → key(32) ‖ nonce(12)

• Message AEAD: ChaCha20P.Enc(key, nonce, padded_plaintext, aad = 0x01 ‖ "ncp1/msg" ‖ session_id ‖ enc_header) — the leading 0x01 is the transport version byte (§8), bound in so a reframing/downgrade can't strip it. mk is single-use ⇒ the deterministic message nonce is safe; session_id in the key-expand info adds defense-in-depth.
• Header AEAD: XChaCha20P.Enc(HKs, random_nonce(24)[prepended], pad(CBOR{dh_pub,pn,n,pq}), aad="ncp1/hdr"‖session_id) where pq = {epoch:uint, pk?:bytes(1184), ct?:bytes(1088)} (§7.5; pk and ct absent when the chain carries none) and pad() is ISO/IEC 7816-4 padding to the fixed HDR_CAP = 2400 bytes, so the encrypted header is always 24 + 2400 + 16 = 2440 bytes and a rekey message has no shape (Round-4 an earlier issue). The receiver cannot know the counter n before decrypting the header, so the nonce must be random; the 192-bit XChaCha nonce makes reuse under a long-lived per-chain HKs negligible (no message-per-chain cap needed).

7.3 Out-of-order handling

MAX_SKIP = 1000 per chain; skipped-key store capped at 2000 entries/channel, 30-day TTL, evict oldest on overflow. A skipped message key MUST be deleted on first successful use (replay of that envelope then fails). Trial-decrypt order per DR-HE: HKr then NHKr.

7.4 State persistence

Ratchet state (RK, CKs/CKr, DHRs, DHRr, HK/NHK pairs, Ns/Nr/PN, skipped-key map, pq_rekey epoch state §7.5) is CBOR-serialized and stored only encrypted under the channel's working key K_store (§11.2) inside the fixed-slot padded working store; never plaintext on disk; wiped from memory when the Chats gate locks (§11.3). In strong mode (§11.2) it is additionally locked behind the drive and wiped on drive lock. Ratchet state is never vaulted/cloned (would break PCS — §11.4) and never backed up (§11.2). Writes are atomic (temp file + rename, or a SQLite transaction) and MUST complete before ack (§9.2).

7.5 Periodic post-quantum re-injection (pq_rekey, v1)

Why (corrected in Round 4, an earlier issue). Every root key RK_i = HKDF(salt = RK_{i-1}, ikm = dh_i) inherits RK₀, which depends on ss_pq; a future quantum adversary who recorded the traffic recovers every dh_i but not RK₀, so harvest-now-decrypt-later is already defeated for the whole session absent a state compromise (P5). What the classical DH ratchet lacks is post-quantum post-compromise healing: after a snapshot of the ratchet state, a classical DH step does not lock a quantum adversary out again; a KEM step does. pq_rekey provides that, bounded by one epoch. It is the Apple-PQ3 pattern.

Where the material rides (Round-4 F1 — the v2-plan wording "in the encrypted body, mixed at the next ratchet step" was circular with the chain it keys and ambiguous under reordering; it is void). PQ material rides in the DR-HE header (§7.2), which the receiver decrypts under HKr/NHKr before any root step, and it is carried identically on every message of a sending chain, exactly as dh_pub is, so a lost or skipped chain-starter is recovered from any later message of the chain (unchanged MAX_SKIP semantics).

header.pq = { epoch: uint, pk?: bytes(1184), ct?: bytes(1088) }

Initiator (either party):
  MAY include a fresh ML-KEM-768 encapsulation key pk_e when it starts a new sending chain;
  MUST do so if ≥ 50 messages have been sent or 24 h have elapsed since its last pk (whichever first);
  sets epoch = e (per-session counter, starts at 0 after the handshake and after every session_reset);
  retains at most TWO decapsulation keys (current e, previous e−1); zeroizes sk_e immediately after the
  first successful Decaps of a ct for epoch e.
Responder:
  on its NEXT sending-chain start after receiving a pk_e it has not yet answered, MUST include
  ct_e = ML-KEM-768.Encaps(pk_e) with the same epoch e (and MAY include its own fresh pk for a new epoch);
  keeps ss_e until the root step below consumes it, then zeroizes it.
Root step:
  the root step keyed by the dh_pub of the sending chain WHOSE HEADER CARRIES ct_e uses
  KDF_RK_pq(rk, dh_out, ss_e, e, pk_e, ct_e) (§7.2) on BOTH sides; every other root step uses KDF_RK.
  The label difference is the domain separation; presence of pq material is authenticated by the header
  AEAD. This rule is well-defined regardless of message order because the KEM secret is bound to a
  specific chain, not to "the next step".
Errors:
  a ct for an unknown or already-consumed epoch, or a pk that fails FIPS-203 validation, is treated as a
  header-AEAD failure (drop; no state change). A peer that never answers two consecutive pk's → the
  client surfaces an informational "post-quantum refresh not confirmed" (a non-responding peer already
  holds every key; this is a health signal, not a security event).

Implementation clarifications (P1, 2026-09-18 — normative): (1) a sending chain carries at most one of pk / ct; answering an unanswered peer pk takes priority over opening a new epoch, which then waits for the next chain. (2) Epoch ids are disjoint per role so both parties may initiate: the joiner (Alice) uses odd ids 1, 3, 5…; the inviter (Bob) uses even ids 2, 4, 6…; a party MUST reject a pk whose epoch has its own parity. (3) In the Double Ratchet a party's new sending chain is created when it receives the peer's new dh_pub, so the answer (Encaps, KDF_RK_pq on the sending root step) and the cadence decision (open a new epoch if ≥50 of its own messages or ≥24 h since its last pk) happen at receive time; every message of that chain then carries the same pq field, and a receiver MUST reject a header whose pq differs from the first header of the same chain. (4) The cadence counter counts the party's OWN sent messages. Reference implementation: the apps’ ratchet module (37 tests incl. a randomized-schedule property test).

Guarantee (honest): after a compromise of one party's ratchet state, a quantum-capable adversary who stays passive is locked out at the first root step that consumes a KEM epoch whose sk_e was generated after the snapshot — at most one epoch (50 messages / 24 h) plus one round trip. If the pending sk_e was inside the snapshot, healing happens at the second boundary (hence immediate sk_e zeroization). An active adversary can defeat PCS in the Double Ratchet regardless (standard caveat). Approved public wording: "post-quantum at setup; post-quantum recovery after a device compromise within one epoch." Never "fully post-quantum".

Cost: ≤ 2272 B of KEM material inside the fixed 2400 B header (§7.2); no change to the envelope; one Encaps or Decaps per epoch per side, in JS via @noble/post-quantum in v1 (§14).

Verification (Round 5, 2026-09-18 — DONE): modelled in ProVerif (ncp-formal/ncp-pqrekey*.pv): agreement on the root key under a reordering attacker, post-quantum post-compromise healing with a pre-epoch state snapshot plus every DH value leaked, classical negative control leaking as required, hybrid with the KEM secret leaked, and the pending-sk_e caveat reproducing — all as intended. See the formal verification report (published with this spec) Round 5. The P1 feature flag may be enabled once fixtures match.

8. Envelope format (transport unit)

Every queue write is one fixed 16384-byte envelope:

offset 0 : u8  version (0x01)
offset 1 : u8  type    (0x01 join | 0x02 msg)
offset 2 : u16 hdr_len         ; join: 0. msg: MUST equal 2440 (= 24 + HDR_CAP 2400 + 16, §7.2); any other
                               ;   value MUST be rejected (Round-4 an earlier issue: a variable header marked rekey messages)
offset 4 : enc_header          ; join: absent; msg: nonce ‖ AEAD(padded header)
...      : payload             ; join: JoinMsg CBOR; msg: message AEAD ciphertext
...      : (no trailing variable region — see padding rule)

Padding rule (H4 — normative, hides length): the plaintext (JoinMsg CBOR, or message payload) MUST be padded with ISO/IEC 7816-4 padding (0x80 then 0x00s) to the fixed AEAD input capacity before encryption, so the AEAD ciphertext — and thus the whole envelope — is exactly 16384 bytes regardless of content. Implementations MUST NOT emit an envelope whose length or ciphertext boundary varies with content. Payloads that don't fit (≳15.8 KB) MUST use attachments (§10).

Client content payload (inside the message AEAD) is CBOR { t, body…, ts }, t ∈ {text,media,location,receipt,react,edit,del,control,sas} (react/edit/del and the control kinds protect/screenshot since 0.6, §8b, §11.3a). Since 0.6 every content payload (text/media/location) MUST carry mid (16 bytes, CSPRNG, chosen by the sender; the one message identity both ends share) and MAY carry re: {m, o} — a reply to the message whose mid is m; o = true when that message is the SENDER's own. A reply MUST NOT carry any content of its target: the receiver renders the quote from its own copy and shows none when that copy is gone (deleted, expired), so a deletion or a disappearing timer is never undone by a quote. Control/receipt payloads MUST be piggybacked onto already-scheduled message envelopes when possible. Delivery receipts are ON (product decision 17, 2026-10-14 — "Delivered" ticks, like Signal; supersedes the earlier off-by-default rule): after user content (text, media incl. voice, location) is decrypted and stored, the receiver sends one coalesced receipt per channel (1.5 s after the last message, at most 5 s into a stream, ≤ 256 ids of each kind) listing the mids (m, 0.6) and the queue seqs (delivered, for 0.5 senders, who learn their seq from the POST and store it on the row as qs) it received. Receipts are sent quiet (§9.2: no push poke). Never from the chat duress space or any duress session, never for receipts/control/sas/system rows, never for a blocked / ended / handed-off / deleted channel; no read receipts. Receipts go only while the transport is connected (no ratchet step spent waiting) and are dropped after 5 failed sends. Builds before this change read the ids as row ids — retire them. Residual SDA timing exposure (§12.4) accepted with the decision.

Forward compatibility (0.5.1). The payload codec is deliberately strict: an unknown t or control kind MUST be rejected, never partially interpreted (a newer peer cannot smuggle semantics past an older one). A client that receives a payload it does not understand MUST still commit the advanced ratchet state (the decrypt succeeded), MUST store a placeholder row ("Update Nygma to see this message") in that position, and MUST NOT act on any field of the unknown payload. Optional fields added to a known type (e.g. dur on media) are ignored by older clients by construction of the map codec. 0.6: a payload MAY carry ign: true; a receiver that does not know its t / kind then commits the ratchet and stores NOTHING (no placeholder, no receipt). Types introduced after 0.6 that are safe to miss set it. Optional extension fields of known types (mid, re) are read leniently: a malformed one is treated as absent and the message itself is kept.

8b. Message actions (0.6, product decision 2026-10-20)

{ t:"react", ts, m: bstr16, o: bool, e: tstr }          e ≤ 64 UTF-8 bytes; "" removes the sender's reaction
{ t:"edit",  ts, m: bstr16, body: tstr }                body ≤ 12 000 bytes
{ t:"del",   ts, ms: [bstr16] }                        1–50 mids

Receiver rules (normative; mobile reference: lib/ncp/actions-core.ts, applied inside the inbound commit transaction, idempotent, a missing or expired target is ignored):

• react — the target is the message with mid m (o = the sender's own → received here, else sent here); one reaction per person per message, the latest wins.
• edit — only the SENDER's own text message; accepted when edit.ts − target's sender ts ≤ 15 min + 2 min. Both times are the author's clock, so clock skew cancels and an edit that waited offline is judged by when it was made. The latest text replaces the old one; the message shows "Edited". No edit history is kept.
• del (delete for everyone) — only the SENDER's own messages; accepted within 48 h + 10 min on the same clock rule. The message is removed with no trace on either side (no "deleted" line), with its plaintext attachment cache; the sender also deletes the attachment blob early (§10.5).
• Every action must also arrive within window + 7 days of the target on the receiver's own clock (a back-dated ts cannot reach into old history).
• A message that never left the sender's phone is edited / cancelled in its send queue; nothing goes on the wire.
• Limits, disclosed in the app: delete for everyone cannot recall what the other person already copied, saved to a drive or photographed; notifications never contain content, so nothing lingers in the notification shade.

8a. Location payload (0.5.1)

{ t:"location", ts, lat: int, lng: int, acc?: uint, label?: text }

lat/lng are signed micro-degrees (round(deg × 10⁶); CBOR here carries no floats), bounded ±90 000 000 / ±180 000 000; acc is the reported horizontal accuracy in metres; label is text the sender typed (≤ 200 bytes), never a reverse-geocoded address. v1 is static only — one fix, taken when the user chooses "Location"; there is no live-location stream. The payload rides inside the ratchet AEAD like text; it never becomes a blob. Rendering is the receiver's choice and is a privacy setting (§12.14).

Envelope cost (documented decision): a 16 KiB fixed size costs ~32 KiB round-trip per message (~280 MB/month for a 300-msg/day user). This is the SimpleX-precedented price of length-hiding (P8). v1 ships a single 16 KiB tier for maximum uniformity; a second smaller tier (e.g. 4 KiB) is reserved (§15) as an explicit size-vs-savings trade (a 2-bucket length oracle for ~4× savings) — not a silent default.

9. Queue protocol (mailbox server)

0.6 additions (§9.2): POST queue/{qid} MAY carry x-ncp-quiet: 1 — published to a live WebSocket, no push poke (receipts, edits, deletes: nothing anyone needs a notification for; before 0.6 every receipt made the other phone show "New activity"). Metadata cost, accepted: the server can tell quiet envelopes from others, which makes receipt traffic easier to pair with the messages it acknowledges (§12.4). DELETE blob/{blob_id} with x-ncp-btok (§10.5). Client side (§11.2): every send of a channel — messages and actions — goes through ONE durable FIFO queue, persisted as intents (sealed), so an action can never overtake the message it names and a send survives a restart; an item is encrypted when first flushed and that envelope is reused for its retries.

9.1 Trust, auth, and the honest linkage story

• A queue is unidirectional: one owner (reader), one writer.
• Send path carries NO account authentication — POST /q/{qid} authorizes solely by the 32-byte bearer wtok. Servers MUST ignore any session/Authorization on this endpoint.
• Receive path authenticates with the queue's otok (32-byte owner token), not the account session.
• Quota (v1): per-account create-rate. Queue and upload creation are account-authenticated in v1 but the server stores no account → qid mapping; it records only a rolling per-account counter ncpquota {accountId, day, created} (a live queue count cannot be decremented on destroy, which carries only otok, so counts are never kept). Disclosure line: "Nygma can count how many chats you started, not which." Blind quota tokens (Privacy-Pass-style, unlinkable) are reserved for v1.x (§15) and remove even the create-time account knowledge.
• Honest limit (P7, §12.1): even with blind quota and account-less sends, a malicious/compelled server that logs IPs can correlate the two queues of a channel by source-IP + interleaved timing and re-link both parties — no cryptography prevents this at the network layer. The claim is minimization, not structural avoidance; Tor/proxy support (roadmap, §15) is what actually closes it. Servers SHOULD keep IP/connection logs ≤ 72 h and MUST publish retention + what is producible (§12.10). Clients SHOULD add randomized send/poll jitter to blunt timing correlation.

9.2 Operations

Delivery persistence (normative): a client MUST persist the raw ciphertext envelope to encrypted local storage before calling ack. Acking on fetch (before durable persist) is forbidden — there is no other copy. WS reconnect MUST resume with recv(cursor) then subscribe; duplicates are tolerated (DR counters dedup).

Receive time (0.5.2, an earlier issue — product decision 2026-10-10): the recv body is {envelopes: [{seq, data, at}], next, now}. at is when S stored the envelope (epoch ms, coarsened to whole seconds); now is S's clock when it answered (epoch ms). Both sit outside the ciphertext and add no new information to S: it wrote the row and already knows when (it keeps that time for the 30-day TTL anyway). A client computes offset = now − local_now when the response arrives and SHOULD display a received message at min(at − offset, local_now) — the server's arrival time on the receiver's own clock — so neither the sender's nor the receiver's clock has to be right, and the disappearing-message timer (§11.4) counts from the same time. The payload ts (§8) stays as it is, is still authenticated by the ratchet, and MAY be kept locally beside the display time; it is no longer what the receiver shows. Own messages show the local send time. A client MUST fall back to the payload ts when at/now are absent (an older server). Order is unchanged: rows sort by arrival (seq). The WebSocket hub carries pokes only, so recv is the one place the time is delivered.

Push: on send, S emits a data-only poke to the product team's registered device token carrying the queue's opaque label and no content. To reduce the send→deliver timing oracle (§12.4), S SHOULD batch/jitter pokes per device. Client display tiers (§11.3): content-free (default) — "Nygma · new activity", nothing decrypted; name only — the client maps label → channel locally, zero decryption, both platforms; name and message — the client fetches and decrypts (Android: headless handler; iOS: Notification Service Extension with a native DR-HE receive path sharing the working store through an app group, v1 product decision 2026-09-18). Delivery is best effort: WebSocket while foreground, poke when the OS allows, full recv(cursor) on app open. In a duress session (§11.3) and in strong mode while the drive is locked, notifications for the affected channels MUST be suppressed locally and content stays in the mailbox. Servers send pokes through the existing Firebase project (FCM data-only, high priority; APNs via FCM with mutable-content). No separate relay service: the WebSocket upgrade path lives in the existing HTTP server (server.js), authenticates with otok in the first frame (never in the URL), and clients tolerate socket drops on deploys by resuming with recv(cursor).

10. Attachments

1. fk ← random(32); content encrypted in 1 MiB chunks: subkey = HKDF(fk, ∅, "ncp1/att/content:"‖blob_id, 32), deterministic per-chunk nonce = LE32(chunk_index) ‖ 0⁸ (guaranteed-unique — avoids the random-IV-under-repeated-key shape of the prior ZK IV-reuse bug), aad = "ncp1/att:"‖blob_id‖":"‖chunk_index. Total size is Padmé-bucketed with a random tail before chunking. Thumbnails: separate blobs under "ncp1/att/thumb:"‖blob_id.
2. Upload via blob_put with a grant charged to the sender's quota (§9.2), through dedicated /api/ncp/blob/init|complete endpoints issuing presigned multipart URLs under an ncp-blobs/ prefix with a 30-day lifecycle rule. The existing drive upload route is drive-bound (drive prefix, file rows, plan limits) and MUST NOT be reused; the existing streamer is reused, parameterised with {chunkSize = 1 MiB, nonceFor(i), aadFor(i), subkey}.
3. Pointer message (t:"media", inside the ratchet AEAD): {blob_id, fk, size, mime, name, thumb?, dur?}. dur (0.5.1, optional, seconds) lets a voice note show its length before the blob is fetched; it is the only content hint besides size, and size is already Padmé-bucketed on the wire. thumb is ONE small encrypted preview (≈240 px JPEG, ≤ 10 KB, under "ncp1/att/thumb:"‖blob_id) carried inline in the 16 KiB envelope so a media message renders without a second fetch. True name/size/mime exist only inside message ciphertext. The sender's drive name is never transmitted.
4. Blob lifetime: blobs live TTL 30 d. Because references live only in E2EE messages the server can't read, there is no server-side pin; instead a client that vaults a media message (§11.4) MUST re-encrypt+store the attachment as a drive artifact at vault time (the drive copy, not the mailbox blob, is the durable copy). Non-vaulted media beyond 30 d is expected to expire — disclosed in-app.
5. Vault-native send: a file already in a drive is decrypt-streamed and re-encrypted under fk via the #98 streaming pipeline (20 MiB windows); no plaintext staging. 5a. Early delete (0.6, delete for everyone): at blob/complete the sender MAY register delHash = SHA-256 of a 32-byte delete token it keeps on its own row (never in the pointer). DELETE blob/{blob_id} with the token in x-ncp-btok removes the objects and the row at once (204; also when already gone); a wrong / missing token or a blob registered without one → 403 (it expires at 30 days). The receiver holds the blob_id but never the token. delHash is set when the row is created and never replaced.
6. Size (0.5.3, product decision 2026-10-16): the largest attachment is the sender's plan's largest file (the same maxFileSize as drives: 100 MB … 2 GB), applied by the sending app before anything is read — the server cannot tie a blob to the sender's plan without linking chats to the account (§9.1); its ceiling stays BLOB_MAX_CHUNKS = 2048 × 1 MiB (a 2 GiB file pads to exactly 2048 chunks). Both directions stream one chunk at a time. Presigned chunk URLs (PUT 30 min, GET 15 min) are re-requested during a long transfer — the same calls for the same blob_id and chunk count. Receiving and viewing are never plan-limited; saving into a drive follows the drive's limit.

11. Drive binding, the working store, duress, and history

Round 4 replaced the July "everything under the drive key" model with a two-key model (design plan v2.1 §2; product team decisions 2026-09-18). The vault side stays under the drive; the live side lives under a per-device working key so chat behaves like a messenger. This section is normative for both.

11.1 The channel record (vault side) and the per-drive container

Every channel belongs to exactly one drive. The channel record — {channel_id, record_version, lease {device_id, device_label, leased_at}, peer profile, tier, IK_J/IK_I keys, peer IK_pub, queue refs + tokens (wtok AND otok), settings, notification mode, strong_mode} — is stored inside one fixed-size padded container per drive, artifact ncp-channels (baseKey = drive metadataKey, artifactType="ncp-channels", fixed slot count × fixed record size, random filler, rewritten as a unit), present on every drive including decoys from drive creation. A compelled server therefore cannot count a drive's channels from artifact rows (Round-4 F9; the per-channel ncp-channel artifact of 0.4 is withdrawn). record_version is monotonic and bound into the artifact AAD (v2:<driveId>:ncp-channels:<version>); a device MUST reject a container whose version is lower than the highest it has seen (server rollback defence). channel_id/message_id MUST be drawn from a namespace that cannot collide with drive-file fileIds.

Re-vault invariant: vaulted queue tokens are always current — every rotate_wtok AND every rotate_otok re-vaults atomically (write the new container, then use the new token). A device that cannot re-vault (drive locked, offline) MUST NOT rotate.

The channel record is what lets a reinstalled device — or another device of the same user — recover channel identities and queue addresses with the drive password (§11.4). It never contains ratchet state.

11.1a The lease: one active device per channel (Round-4 F3, F6, F7, an earlier issue)

Only the device named in lease runs the ratchet, fetches from and sends to the channel's queues. Every other device that opens the drive sees the channel read-only ("Active on <device_label> · Move here") with whatever vaulted history exists.

Approved take-over (normal path). The new device writes lease_request {device_id, label} into the container. The current holder — which alone holds the non-vaulted continuity secret in its device keystore — shows "Move chats to <label>?"; on yes it (1) sends control:superseded{reset_epoch+1} to each peer on the existing trusted ratchet, (2) calls rotate_otok on both queues and re-vaults, (3) writes lease = new device with record_version+1, (4) wipes its working state. The new device then runs session_reset (§11.4) with each peer; peers that received control:superseded MUST NOT raise the Check-again banner. Silent for peers.

Unattended take-over (old device lost, or user chooses "I don't have it"). The new device writes lease, calls rotate_otok on both queues, re-vaults, and runs session_reset with each peer. Peers see the Check-again banner (mandatory SAS for sensitive channels). The previous holder, on its next launch, finds its otok refused and/or a newer record_version, and MUST display "A device called '<label>' took over your chats at <time>. Not you? → Revoke". Revoke = destroy both queues via the vaulted (now rotated — so revoke requires the drive password on the old device, which re-reads the current tokens) and notify peers with control:revoked and with the keyless revoked notice (2026-09-20, an earlier issue): after a take-over the peer has already replaced the ratchet, so control:revoked on the old ratchet is unreadable. The notice is authenticated with the channel identities instead, which both sides hold for the life of the channel: K_rev = HKDF(X25519(IK_mine, IK_peer), ∅, "ncp1/revoke/key:" ‖ channel_id, 32), tag = ChaCha20-Poly1305(K_rev, nonce 0×11‖'R', ∅, aad = "revoked" ‖ channel_id ‖ LE64(ts)), sent as a keyless envelope CBOR{kind:'revoked', channel_id, ts, tag}. A peer that verifies it MUST show "This chat was ended" and stop sending. The old device MUST NOT display a reassuring "moved" message.

Rules.

• A device whose otok is refused, or that receives control:superseded, MUST stop fetching and sending immediately and re-read the container.
• After any rejected reset_init a device MUST re-read the container and stand down if the lease is not its own; reset_resp carries the peer's last_accepted_reset_epoch for counter re-sync.
• Two devices that both see no lease (first open) race: the first rotate_otok wins at the server; the loser's fetch is refused and it stands down. This is why enforcement is server-side, not policy.
• The lease record is inside the AEAD'd container; the server learns nothing from it except the write pattern (mitigated by the fixed-size container).
• Web has no chat in v1; it may display vaulted history read-only and never takes a lease.

11.2 The working store (live side): K_wrap → K_work → K_store

K_wrap   hardware-backed wrapping key. Android: AES-256-GCM in AndroidKeyStore, StrongBox if available,
         TEE otherwise; NO setUserAuthenticationRequired; NO setUnlockedDeviceRequired (a push that
         arrives with the screen locked must still decrypt). iOS: keychain item with
         kSecAttrAccessibleAfterFirstUnlockThisDeviceOnly in a shared keychain access group (the
         notification extension reads it). Non-exportable.
K_work   32-byte software key generated at first launch on EVERY installation (whether or not a chat
         exists), stored wrapped under K_wrap. Never synced. Never backed up (android:allowBackup=false /
         fullBackupContent exclusions; NSURLIsExcludedFromBackupKey). Present in process memory whenever
         the app runs; that is stated, not hidden.
K_store  per channel: HKDF(K_work, ∅, "ncp1/work/store:" ‖ channel_id, 32). Encrypts the ratchet-state
         row (§7.4), the message cache and the channel index. At-rest records follow the ZK-v2 artifact
         scheme (per-artifact HKDF subkey, fresh IV, AAD) — one IV, one plaintext, forever.

The working store is a single fixed-slot padded container (64 slots × fixed record size, random filler, rewritten as a unit; the message cache in fixed-size pages) in SQLite, present from first launch, so slot count, sizes and modification times reveal nothing about how many channels exist or which are active. It MUST NOT be kept in a small-value secure store.

Strong mode ("Require the vault password for Chats", set in Security Hub; shipped 2026-09-20): the account's Chats vault (the hidden purpose='chats' drive) gets a user-chosen password — the client proves the current KDF-v3 verifier and sends the new verifier plus the content/metadata keys re-wrapped (wrap v2) via PUT /api/drives/{id}/keys; the server stores ciphertext and one-way verifiers only, and the device-random convenience password is forgotten. The REAL space then uses its own working key K_real (random 32 B) stored only as nonce24 ‖ XChaCha20-Poly1305(KEK, K_real, aad = "ncp/strong:" ‖ account_id) with KEK = HKDF(K_meta[chats drive], ∅, "nygma-mobile/ncp/strong/kek", 32); every real-space row (container, slots, messages, inbox, pending) is re-keyed from the keychain K_work to K_real in one SQLite transaction. K_real exists in memory only after the gate's second step (PIN → vault password → unlockDrive → unwrap) and is forgotten, with the vault locked, on every gate lock. The decoy space keeps the keychain K_work, so the duress PIN still opens a plausible empty app with no password step. No background decrypt, content-free notifications, channels visible only while the vault is open. This is the only mode in which hidden channels are cryptographically inaccessible while the phone is locked. Turning it off needs the password: rows are re-keyed back and the password is stored again for convenience mode. The earlier per-drive wording ("K_work[drive] = wrap_v2(K_drive, …)") is superseded: there is one Chats vault per account, and the wrap is under a key derived from its metadata key, not under the drive password directly.

Because K_wrap is not credential-gated, the PIN/biometric gate of §11.3 is app-enforced. This is stated plainly in P9 and in the published threat model (§12.3, §12.13).

11.3 The Chats gate and duress behaviour (normative)

• Gate. The Chats tab opens with the Nygma PIN (one PIN for the app shell and for Chats; per-drive quick-access PINs are unchanged). Biometric unlock is an opt-in shortcut, off by default for Chats. The gate re-locks after a background period (user-configurable 0 / 30 s / 1 min / 5 min; default 1 min, owner decision 2026-09-24; outside activities the app itself opens — camera, pickers, share sheets, permission screens — never count), MUST NOT fail open, and is disabled (chat unusable) until a PIN is set. A "Lock chats now" action exists. The PIN verifier is keystore-bound so an extraction cannot brute-force it offline.
• Duress PIN. The existing two-slot PIN store is reused: slot 1 = real PIN, slot 2 = the existing duress PIN (always present as random filler when unset, keystore-bound, uniform shape). Entering the duress PIN at the Chats gate — or entering the duress password on a drive — sets ONE session-wide duress state that persists until the user passes the locked gate again with the real PIN. Real-PIN entry from inside a duress session is not offered; the session must lock first.
• In a duress session the client MUST: (1) filter the channel index to channels whose owning drive is a decoy — real channels are absent, never "locked"; (2) render the Chats tab as the first-run state, pixel-identical to a never-used installation (default decoy; decoy channels with consenting peers are an advanced option); (3) clear delivered notifications (best effort) and suppress new local notifications for non-decoy channels — the headless/push handler reads the persisted duress flag before posting anything; (4) call push_mute with jitter (the same endpoint backs "Pause notifications"); (5) show no counts anywhere (app icon badge never shows a number; tab badge is a dot); (6) leave real-password-on-real-drive behaviour exactly as today. Any account/quota UI MUST NOT display channel or queue counts.
• Notifications. Default content-free. "Name only" (via the queue label, §9.2) and "name and message" are per-drive opt-ins behind a disclosure that Android keeps a 24-hour notification history the app cannot clear and iOS keeps delivered notifications until cleared. Previews never contain a drive name. Chat screens are hidden in the app switcher; screenshots follow the device setting "Block screenshots" (default OFF, product decision 2026-10-16) unless the chat is protected (§11.3a).
• Protect this chat (§11.3a, 0.6, product decision 2026-10-20). Each person has their own flag (control:protect {on}, kept in the channel record as pm mine / pp peer, vaulted, re-sent after a session reset). The chat is protected while EITHER flag is on — strictest wins — and only its product team can turn a flag off. While protected, both phones block screenshots and screen recording (Android FLAG_SECURE; iOS secure layer + a black view while the screen is captured) whatever the device setting, and offer no Copy, Save to drive or Open with. On iOS a screenshot that still happens is reported: control:screenshot → "X took a screenshot" on both phones (≤ 1 per 10 s; never from the duress space). Honest limit, disclosed: it cannot stop another camera.
• Free plan. The duress PIN and the decoy Chats state are available on every plan (product decision 2026-09-18); with "decoy = first-run" they cost nothing.
• Honest limits (elevated to P9, disclosed in §12.3/§12.13): default mode hides, it does not lock — a coercer with the device passcode and forensic tooling reads every channel's working state; strong mode restores cryptographic inaccessibility at the cost of background delivery; OS notification history when "name only" was opted in; per-drive artifact counts are hidden by the fixed-size container but the container's write pattern remains visible; push_mute calls are visible to the server (covered by the "Pause notifications" feature).

11.4 History (ephemeral by default, opt-in vault) & reinstall recovery

History. Default: messages live in the encrypted local cache under per-channel disappearing timers (enforced both ends via control). Opt-in per channel (either side, visible to both): messages are additionally written to the drive as v2 artifacts (artifactType="ncp-msg", fileId=message_id, batched); vaulted media follows §10.4. Documented trade-off (also in-app): vaulted copies are outside the ratchet's FS — protected instead by the drive's crypto + duress invisibility.

Reinstall = session reset, not a dead channel. Because IK_J, the peer's IK_pub, and the queue refs+tokens are vaulted (§11.1) — but ratchet state is not (never cloned) — a reinstalled device recovers its channel list and re-establishes each channel without an out-of-band meeting, via the session_reset re-handshake below. A reinstall onto a device that is not the lease holder is a take-over and follows §11.1a (approved or unattended); session_reset is the cryptographic step of both.

Round-2 REDESIGN. Draft 0.2's reset was a one-sided, single-message, static-authenticated derivation (SK' = HKDF(… X25519(IK_restored, IK_peer) ‖ X25519(EK_new, IK_peer) ‖ EK_peer_pub? …)). Adversarial review found it broken on every axis: replayable (all inputs static/reproduced → a relay re-posting a captured reset re-derives an identical SK', tears down the live ratchet, and restarts the deterministic-nonce sending chain at counter 0 → ChaCha20-Poly1305 (key,nonce) reuse + Poly1305 forgery + permanent DoS); no forward secrecy (both classical DH terms anchor on the peer's static IK — a later IK_peer_priv leak recomputes the whole classical secret; there was no ephemeral×ephemeral term — the literal EK_peer_pub? was the missing peer contribution); no KCI resistance (symmetric X25519(IK_A,IK_B) = X25519(IK_B,IK_A), so a leak of the peer's own IK_priv lets an attacker impersonate any third party to that peer forever); PQ-downgraded (a one-message reset cannot carry a mutual ss_pq', silently dropping the §2 hybrid MUST → harvest-now-decrypt-later returns on every reinstall); and under-specified (no reset transcript, no §13 label, so the re-verify SAS meant to catch all this might not even bind the new keys). It is replaced by the following.

session_reset — a two-message, mutually-ephemeral, hybrid-PQ, epoch-bound, key-confirmed re-handshake. The restored device is Alice-role (sends first). Both messages ride the existing q_join/q_reply (framed as §8 keyless type 0x01, kind = reset_init / reset_resp), and a receiver MUST NOT touch its live ratchet until key-confirmation succeeds (step 4).

per-channel reset_epoch : monotonic counter in the vaulted ncp-channel artifact (§11.1); the peer
  persists last_accepted_reset_epoch and MUST reject any reset_init whose epoch ≤ it (anti-replay).

1. reset_init  (restored A → peer B):  { channel_id, reset_epoch, N_A(16),
                                          EK_A(32, fresh X25519), kem_A(1184, fresh ML-KEM enc key) }
     — authenticated implicitly: only the IK_A holder can complete step 3/4. No ratchet action yet.
   B, on receiving reset_init, generates its own fresh EK_B + N_B, runs Encaps(kem_A), and derives
   SK' (step 3) — so it can already key-confirm in reset_resp. B does NOT reset its ratchet yet.
2. reset_resp  (peer B → A):           { channel_id, reset_epoch, N_B(16),
                                          EK_B(32, fresh X25519), kem_ct(1088 = Encaps(kem_A)),
                                          confirm_B = AEAD(confirm_key, "B", reset_transcript) }
     — confirm_B is B's key-confirmation. **It is MANDATORY and load-bearing** (see the Round-3
       machine-check note): without a B→A confirmation, A is not authenticated to B's identity — an
       attacker who substitutes reset_resp impersonates B to a reinstalling A. A MUST verify confirm_B
       before completing (step 4). B still does NOT reset its ratchet yet.
3. Both derive, with FRESH ephemerals on BOTH sides + a real ephemeral×ephemeral term + a KEM secret:
     reset_transcript = SHA-256( "ncp1/reset" ‖ channel_id ‖ LE64(reset_epoch)
                                 ‖ IK_A_pub ‖ IK_B_pub ‖ EK_A ‖ EK_B ‖ kem_A ‖ kem_ct ‖ N_A ‖ N_B )
     RD1 = X25519(IK_A_priv, EK_B)      ; binds A's identity to B's fresh ephemeral (KCI-resistant)
     RD2 = X25519(EK_A_priv, IK_B_pub)  ; binds B's identity
     RD3 = X25519(EK_A_priv, EK_B)      ; ephemeral×ephemeral → forward secrecy
     ss_pq' = Decaps/Encaps(kem_A)      ; genuine two-party KEM secret (both hold it after the round-trip)
     SK' = HKDF( ikm=0xFF×32 ‖ RD1 ‖ RD2 ‖ RD3 ‖ ss_pq', salt=∅,
                 info="ncp1/reset/sk" ‖ reset_transcript, len=96 )
         = RK₀'(32) ‖ session_id'(32) ‖ sas_seed'(32)
     confirm_key = HKDF(SK', ∅, "ncp1/reset/confirm" ‖ session_id', 32)
     ; confirm_X = ChaCha20-Poly1305(confirm_key, nonce = 0x00×11 ‖ byte('X'), plaintext = ∅,
     ;                               aad = reset_transcript) → the 16-byte tag   (P1 clarification: 'A' = 0x41, 'B' = 0x42;
     ;                               confirm_key is single-use per reset, the two nonces are distinct)
4. MUTUAL key-confirmation BEFORE any ratchet re-init:
     - A first verifies B's confirm_B (from reset_resp); on failure ⇒ drop, keep the OLD ratchet.
     - A then sends reset_confirm = AEAD(confirm_key, "A", reset_transcript).
     - B verifies A's confirm; only then do BOTH re-initialize the ratchet from SK' (§7.1 roles:
       A=Alice, B=Bob) and persist the new reset_epoch.
     Any AEAD/confirm failure ⇒ drop silently, keep the OLD ratchet intact (never tear down on an
     unproven or replayed reset). The MUTUAL confirmation is what makes the reset authenticate in
     BOTH directions — ProVerif confirms `A↔B` injective agreement holds only with confirm_B present.

• The peer surfaces a prominent key-change / "Check again" banner (tier → Check again, §4) with the composer disabled until the user acts, and a mandatory 8-word SAS gate for sensitive/duress channels (a nudge only for low-sensitivity ones). 0.5.3 (product decision 2026-10-16): replaced by one quiet system line in the thread and no blocked composer (§4); a Verified channel returns to Connected. sas = HKDF(sas_seed', ∅, "ncp1/reset/sas" ‖ reset_transcript, 11). Exception: if the peer received an authenticated control:superseded{epoch} on the old ratchet before this reset (an approved take-over, §11.1a), it MUST NOT raise the banner; the old device vouched for the new one.
• reset_resp additionally carries B's last_accepted_reset_epoch so a device that lost a reset race (§11.1a) can re-synchronise its counter instead of falling to OOB re-pair (Round-4 an earlier issue).
• Reset must not depend on a stale token: §11.1 mandates vaulted queue tokens are always current (atomic re-vault on every rotate_wtok). If the cached wtok is nonetheless dead, the reset falls back to explicit OOB re-pair rather than black-holing.
• PCS is honest now: it comes from the mandatory fresh mutual ephemeral (RD3) whose private keys the attacker never held — NOT from "state was never cloned" (that only preserves the old session's FS; deleted from the spec as a non-sequitur).
• Stolen-vault caveat: a coercer who extracts a real-drive IK_priv (or holds the drive password) can still initiate a reset — and, since 0.5, an unattended lease take-over (§11.1a). The peer sees the key-change banner + SAS prompt (same class as Signal's stolen-identity-key case) and the previous device shows a take-over alert with Revoke on its next launch; it is never told a reassuring "moved". For a silent reset NCP additionally requires the non-vaulted continuity secret held in the device keystore (never written to the §11.1 record), which only the current lease holder has; a vault-only recovery is therefore always loud. A decoy-drive extract yields nothing.
• Undecryptable pre-reset backlog is surfaced as "N earlier messages couldn't be recovered."
• Duress interaction (§11.3): re-establishment MUST be de-bursted (randomized jitter, lazily per-channel on first use) and the reset envelope MUST be wire-indistinguishable from a 0x02 msg (same 16 KiB framing, same constant hdr_len) so a compelled server cannot bucket a decoy-unlock burst vs a later real-unlock burst by push-token/IP/timing to label hidden channels — see §12.9b.

12. Security considerations

1. Malicious server. Cannot: learn keys/plaintext, substitute invitation blobs (AEAD), forge messages, or silently MITM at bootstrap (P2). Can: drop/delay/reorder (availability); via IP+timing correlate a channel's two queues and re-link both parties (P7 limit — mitigations: account-less sends, jitter, Tor roadmap, blind quota v1.x); count how many queues an account created (v1 create-rate quota, §9.1 — disclosed); observe message counts/arrival (length hidden by §8); refuse or roll back the channel container (bounded by record_version, §11.1); force a reset by dropping traffic (visible as a Check-again banner).
2. Link interception (Connected). Passive view of a used link → nothing. Winning the race to fetch first locks out the real joiner, who sees CLAIMED — detectable by the joiner, not the inviter (the inviter sees a successful join). With the claim code (§5.3) a link-only attacker also needs the second channel; three wrong codes burn the link visibly to the inviter. Active replacement of link (and code) before first open → full MITM until SAS (§5.5). Bounded by the mutual SAS and the one-time verify nudge.
3. QR substitution (Verified). Requires controlling the display/camera at ceremony time and surviving the reverse-scan transcript check — i.e., endpoint compromise (out of scope).
4. PCS limits. Healing needs a fresh, unobserved DH ratchet round-trip; skipped-key caches (§7.3) extend exposure by design; an IK-holder can impersonate within the channel until re-verification — surface key-change/reset events prominently (§11.4). Push pokes create a send→deliver timing oracle (SDA, ~5 messages in the literature) — mitigated by poke batching/jitter (§9.2) and coalesced receipts (§8; on since 2026-10-14 by product decision — the remaining send→deliver timing signal is accepted and disclosed).
5. SAS grinding. ~2⁸⁸ against a single-use invitation (§5.5); single-use is the load-bearing invariant; partial comparison is a break (UI forbids it).
6. Deniability. Offline deniability of content: no signatures anywhere; the KEM keys are ephemeral and unsigned (so the published PQXDH deniability caveats about signed long-term KEM prekeys apply less here, not more); confirm_B, reset_confirm, control:verified and control:superseded are MACs under keys both parties can compute → simulatable. Not claimed: online deniability; deniability of participation — account-authenticated queue creation and push registration are server records. Say "content deniability yes, participation deniability no".
7. Replay. Invitations: single-use inv_id + one-time blob lock. JoinMsg: dedup distinct msgs; retransmit identical (§6.4). Messages: DR counters + delete-skipped-key-on-use (§7.3).
8. Downgrade. Version is bound in transcript (whole invitation hashed); peers MUST reject other versions, never negotiate down.
9. Quantum (corrected in Round 4, an earlier issue). Handshake AND session-reset are hybrid, and every Double Ratchet root key is derived from the previous one, so every session key inherits the ML-KEM secret: recorded traffic is not decryptable by a future quantum adversary absent a device-state compromise. The classical DH ratchet means a quantum adversary holding a state snapshot can read messages until the next pq_rekey epoch (§7.5: ≤ 50 messages / 24 h + one round trip; passive adversary; epoch key generated after the snapshot). The 0.4 sentence "could break post-appearance messages" was wrong and is withdrawn. 9b. Reinstall reset-burst vs duress (disclosed). Blind quota (§9.1) blinds only create-time account→qid; it does NOT blind the device/push-token grouping. A reinstall re-establishing many channels produces a burst a compelled server could bucket (decoy-unlock vs later real-unlock) to infer hidden channels. Mitigated (not eliminated) by de-bursting/jitter + wire-indistinguishable reset envelopes (§11.4) + per-drive push-token rotation; disclosed in §4.7/P9. 9d. Account-linked message tokens (disclosed, product decision 2026-10-23). For admin messages (offers, news, service notices — /admin/messages) the app registers its FCM token WITH the signed-in account (pushtoken table). The same token may also be the push token of the device's chat queues (ncpqueue.pushToken, ncppushdevice, still never account-linked), so a compelled server can now join account → token → that device's queues, i.e. learn which queues an account's phone reads (not with whom, not the content). Chosen knowingly over FCM topics (no tokens on the server) for exact targeting and counts. The chat tables are unchanged; a later hardening is a second FCM sender id for messages (a different token per purpose). Public claims must not say the server cannot link an account to its chat queues. 9c. Persistent qids link devices across reinstall (disclosed). Per-channel queue IDs are stable pseudonymous identifiers; a reinstall drives the identical qid pair from a new IP/device, so an IP-logging server can link old↔new device. Disclosed in the §4.7 threat table; optional fresh-qid migration inside session_reset is reserved (§15).
10. Metadata honesty. The §4.7 threat table in the design doc is normative marketing collateral; public claims MUST NOT exceed it (FTC v. Zoom; UK ASA — never "most secure").
11. Long lock/coercion vs 30-day TTL. A user locked out or coerced > 30 days silently loses queued messages. Disclosed in-app; TTL extension MAY be a paid-plan option.
12. DoS surfaces. wtok flooding (bounded by per-queue rate + storage caps + mandatory rotation, §9); blob_put exhaustion (bounded by grants + size/IP caps, §10); trial-header CPU (bounded by rate limits + MAX_SKIP, §7.3); claim-code burn (requires the link; the loud burn is the intended outcome); envelope must be stored in object storage, not an InnoDB row (16 KiB > page → off-page churn).
13. Duress default mode hides, it does not lock (Round-4 F4). K_wrap is not credential-gated (§11.2); a coercer with the device passcode plus forensic tooling reads every channel's working state, hidden ones included. Nygma's drive duress does survive that (the real drive key is password-derived and absent from the device); chat's default mode does not, and marketing MUST never blend the two. Strong mode (§11.2) restores the drive-class guarantee.
14. Client-code trust. The "no key server" guarantee is strongest in the native apps (store-signed, reproducible Android build). A web client runs code the server delivers; v1 chat is mobile-only for this reason, and web chat (v2) ships with subresource integrity and a signed bundle manifest.
15. Lease take-over by a vault holder (§11.1a). Possible by design for recovery; made loud on the previous device and at the peer (Check-again banner) unless the previous device approved it. Server rollback/withholding of the container is bounded by record_version and by server-side otok rotation; the failure mode is a refused fetch, never a silent fork.
16. OS notification history. With "name only" opted in, Android's 24-hour history and iOS's Notification Center retain names the duress session cannot remove; the default is content-free and the opt-in carries this disclosure (§11.3).

12.14 Map previews for location messages (client-side, opt-in)

A location message renders by default as coordinates + accuracy + the sender's label, with "Open in Maps" as an explicit user action — nothing about the point leaves the device until then. The receiver MAY turn on map previews (Security Hub › Chats, off by default). With it on, the client fetches one map tile (z = 15, ≈ 1.2 km square) per location message directly from the tile provider configured at build time (EXPO_PUBLIC_MAP_TILE_URL, e.g. a keyed MapTiler/Stadia endpoint serving OpenStreetMap data; the public OpenStreetMap servers block app traffic under their usage policy, so they are not used). Without a configured provider the switch is disabled and says so. What the provider learns: the receiving device's IP and the tile (a ~1 km² area) at fetch time, plus the app's key. What it cannot learn: who sent the point, which chat, the exact coordinates, or the label. The setting text states this plainly; required attribution is shown on the tile. Senders are not told whether a receiver has previews on. No Google/Apple map SDK is embedded.

13. Domain-separation label registry (v1 — no additions without a spec bump)

ncp1/invblob/id, ncp1/invblob/key, ncp1/invblob/poll (HKDF, §5.3), ncp1/invblob(aad), ncp1/claim (HMAC, §5.3), ncp1/hs, ncp1/hs/sk, ncp1/jmwrap, ncp1/jm(aad), ncp1/sas, ncp1/hk0, ncp1/rk, ncp1/pqrk (HKDF info, §7.5; spelled without a slash so that ncp1/rk is not its prefix — the P1 label test enforces §13's prefix-freedom mechanically), ncp1/mk, ncp1/msg(aad), ncp1/hdr(aad), ncp1/att/content:*, ncp1/att/thumb:*, ncp1/att:*(aad), ncp1/work/store:* (HKDF, §11.2; replaces ncp1/store:*), ncp1/reset (reset transcript prefix), ncp1/reset/sk, ncp1/reset/confirm, ncp1/reset/sas; header field pq (§7.2); at-rest artifactTypes ncp-channels (per-drive container, §11.1; replaces ncp-channel), ncp-msg (existing v2 AAD scheme), with the record_version AAD extension v2:<driveId>:ncp-channels:<version>. Removed in 0.5: ncp1/pqrk, ncp1/lease (the lease is inside the AEAD'd container; no separate label).

Injectivity (corrected in Round-2): within each primitive's input namespace — AEAD associated-data, HKDF info, and hash-transcript prefix — the labels are pairwise prefix-free, so label ‖ variable is unambiguous (and inv_id/channel_id are fixed-length). Textual prefixes that appear across namespaces (ncp1/jm ⊂ ncp1/jmwrap; ncp1/hs ⊂ ncp1/hs/sk; ncp1/reset ⊂ ncp1/reset/*) are harmless because the two members of each pair are never inputs to the same primitive and labels are constructed at fixed call sites, never runtime-parsed. (The draft-0.2 blanket "no prefix is a prefix of another" was literally false; this is the accurate property.)

14. Implementation mapping (informative)

• the apps’ shared protocol library — protocol core on the existing CryptoPrimitives pattern; new primitives via @noble/curves (X25519) + @noble/post-quantum (ML-KEM-768); byte-parity proven web↔mobile by the ZK-v2 fixture harness. All X25519/ML-KEM validity checks (§2) implemented explicitly, not left to the binding.
• RN production notes (corrected in Round 4): (a) CSPRNG health-check gate — before ANY keygen, run a runtime self-test on the app's actual randomness source (expo-crypto getRandomValues bound into noble's randomBytes; the app does not use react-native-get-random-values): draw two 32-byte buffers, assert neither is all-zero and they differ, and fail closed. (b) ML-KEM runs in JS (@noble/post-quantum) in v1: no app-facing native ML-KEM exists on Android, iOS CryptoKit exposes it only from iOS 26, and react-native-quick-crypto wraps none. This is acceptable precisely because §2's "classical security MUST NOT depend on ML-KEM" rule is load-bearing; native decapsulation (Nitro module over OpenSSL 3.5) is reserved for v1.x. Benchmark Encaps/Decaps on the mid-range test phone in S0. (c) Working store in expo-sqlite (WAL, transactions), never a small-value secure store; K_wrap/K_work via react-native-keychain (iOS access group, AFTER_FIRST_UNLOCK_THIS_DEVICE_ONLY) or a small Expo Module for the Android StrongBox flag. (d) Push: @react-native-firebase/messaging headless handler on Android; a Notification Service Extension target on iOS (third signed target in the Mac build chain; App Groups + Keychain Sharing entitlements). (e) Camera/QR: expo-camera + react-native-qrcode-svg; CAMERA permission and NSCameraUsageDescription. (f) App Links for /ch on both hosts. (g) Screen hygiene: expo-screen-capture on chat routes.
• Test vectors: port Signal DR + DR-HE vectors; generate NCP handshake/reset vectors from the reference impl; property-based tests for the state machine (out-of-order, replay, lost-ack retransmit, session-reset, restart).
• Server: /api/ncp/* routes in the existing Next.js app; the WebSocket upgrade path in the existing server.js (no separate relay service); firebase-admin for pokes; envelopes in S3 (ncp/{qid}/{seq}) with a 30-day lifecycle plus a TTL cron on the existing CRON_SECRET pattern; Prisma tables ncpqueue {qid, label, otokHash, wtokHash, createdAt}, ncpenvelope {qid, seq, s3Key, createdAt}, ncpinvitation {blobId, blob, exp, claimHash, attempts, state, pollTokHash}, ncppushdevice {token, deviceSecretHash, muted, mutedUntil}, ncpquota {accountId, day, created} — lowercase names, hand-written migration applied with prisma migrate deploy; no writer identity, no account→qid column, ever (blind tokens in v1.x remove even the create-time knowledge).

15. Reserved for future versions

CPace spoken-code pairing (Verified-remote); SPQR-style continuous PQ ratchet (per-message rather than per-epoch, superseding §7.5); blind quota tokens (Privacy-Pass-style, replacing the v1 create-rate counter); an OPRF/PAKE-gated invitation fetch that makes the claim code a cryptographic gate against non-servers; native ML-KEM decapsulation; a 4 KiB second envelope tier; hardware-backed per-channel IK (Secure Enclave/StrongBox, non-exportable); multi-device signed device lists; MLS group channels (RFC 9420, hybrid-PQ cipher suites, basic credentials verified via §5 ceremonies); Tor/SOCKS transport; per-message write-token rotation; fresh-qid migration inside session_reset; oblivious message retrieval for queue read-unlinkability; opt-in commit-reveal "strong verify" SAS.

16. Adversarial review — findings & resolutions

Round 1 (draft 0.1 → 0.2)

Two hostile reviewers (crypto lens; systems/state lens). Verdict: crypto skeleton sound; not implementable as 0.1 due to C1 + claim/spec gaps. All below resolved in 0.2.

Crypto lens

• C1 (critical) — DR init self-contradictory / channel bricks on msg #1. Bob-role inviter had no sending chain yet was told to send chan_ack first; and destroying EK_I_priv at COMPLETED made the first receive undecryptable. → Fixed §6.4/§7.1: joiner (Alice) sends first; inviter retains EK_I_priv until the first ratchet step consumes it; destroys only the ML-KEM key + replay state at COMPLETED; chan_ack is Bob's response.
• H2 — "no key to server ever" broken by cleartext ik_j in JoinMsg. → Fixed §3.1/§6.3: JoinMsg now wraps ik_j/ek_j/profile under WK (derived from a throwaway WK_J DH to EK_I plus ss_pq); relay sees only random points + KEM ct + AEAD. Claim reworded to the precise form.
• H3 — P7 "structural, no edge recordable" false vs IP-logging server. → Reworded P7/§9.1/§12.1 to minimization; added blind quota tokens + jitter; named Tor as the real fix (roadmap).
• H4 — envelope padding ambiguous → length oracle. → Fixed §8: plaintext padded to the fixed capacity before AEAD; ciphertext/envelope exactly 16 KiB regardless of content; variable emission forbidden.
• H5 — DR-HE header keys mis-seeded (4 symmetric instead of 2 crosswise). → Fixed §7.1 with the exact hka/nhkb crosswise assignment.
• M1 — no mandated key validation. → §2 now requires X25519 all-zero rejection + ML-KEM checks.
• M2 — SAS invariant unstated; partial-comparison "graceful" is wrong. → §5.5 makes single-use invitations a security-critical invariant and states partial comparison is a break; UI must require all 8 words (Round-2 raised 6→8; see the Round-2 block).
• M3 — duress leaks via per-account queue count. → §11.3/§12.3 elevate the limit and spec blind quota as the duress mitigation.
• M4 — push poke is a per-message timing oracle. → §9.2/§12.4 batch/jitter pokes; disclose.
• M5 — transcript hashed over re-encoded CBOR. → §2/§6.2 hash received octets, not re-serialize.
• L1 — random-IV-under-fixed-subkey (echoes prior IV bug). → §10 deterministic per-chunk nonce.
• L2 — skipped key not deleted on use. → §7.3 delete-on-use normative.
• L3 — hdr_len unbounded. → §8 bounds-check mandated. L5 — J's Verified transition underspecified. → §5.2 I sends authenticated control:verified. L6 — SAS derived from material incl. RK₀. → §6.2 dedicated sas_seed slice. L7 — header-key nonce reuse volume. → §7.2 documented + ratchet-before-2³² guidance. (L4 CPU-DoS noted in §12.12.)

Systems lens

• Critical/product-killer — reinstall = manual re-pair + silent black-hole sends. → Fixed §11.4 session_reset (vaulted IKs re-authenticate; fresh ephemerals; key-change banner; PCS intact).
• Critical/claims — "no A↔B edge" practically false. → same as H3.
• High — lost chan_ack deadlock. → §6.4 identical-retransmit + ack-resend rules.
• High — invitation wtok never rotated (permanent flood token). → §5.4/§9.2 mandatory rotate_wtok on COMPLETED.
• High — blob_put open/unmetered; TTL "unless referenced" unimplementable. → §9.2/§10.4 blind upload grants + size/IP caps; no server pin — vault re-stores media instead.
• High — generic pokes betray hidden channels under duress. → §11.3 device-level push_mute auto-invoked on duress unlock.
• High — ack/cursor loses messages; WS resume undefined. → §9.2 persist-before-ack + resume from cursor.
• High — iOS background delivery unreliable. → §9.2/§12 honest per-platform delivery model (foreground WS reliable; background best-effort; locked-drive fetch-on-unlock).
• Med — joiner crash burns link / false interception alarm. → §5.3/§5.4 atomic persist + "already opened here" UX. Med — exp enforcement ambiguous. → §5.3/§6.4 server-authoritative states + inviter grace + joiner timeout; orphan-queue GC. Med — subpoenable channel-count. → disclosed in §12.1 + blind quota. Med — 16 KiB cost. → §8 documented decision + piggybacking.
• Low — 30-day TTL vs long lock (§12.11); attacker-chosen srv (§5.1 allowlist); envelope off InnoDB row (§12.12).

Crypto re-review (the second crypto pass, applied into draft 0.2): independently re-derived C1 (both facets — Bob has no sending chain to open with; EK_I_priv must survive to the first ratchet step) — already fixed as C1. It confirmed as sound, do not "fix": the UKS/handshake auth (whole invitation + IK_J‖EK_J‖kem_ct transcript-bound), the concat-then-HKDF PQ combiner (secure if either primitive holds; KEM non-binding not exploitable since kem_ct is transcript-bound), the EK_I double-use (= Signal's SPK reuse), deniability, deterministic message nonce, and the §13 label injectivity. Additional refinements it raised, now applied: header AEAD → XChaCha20-Poly1305 (§2/§7.2; 192-bit random nonce removes the long-lived-HKs birthday concern — a deterministic header nonce is impossible because the receiver can't know the counter pre-decryption); SAS 6→8 words (§5.5; 2⁸⁸ margin; commitment round rejected as incompatible with async invites); session_id MUST NOT be transmitted (§6.2); transport version bound into the message AAD (§7.2); session_id added to the message-key info (§7.2); joiner's first ratchet key MUST be fresh and ≠ EK_J (§7.1).

Round 2 (draft 0.2 → 0.3) — focused pass on the two new key-agreement paths

A multi-agent adversarial workflow (7 attack lenses + 4 web-validation passes + per-finding verification, ~45 agents) on the §6.3 identity-hiding wrap and §11.4 session-reset (the two paths added in 0.2 that had never been independently attacked). 27 findings confirmed/partial, 5 refuted. Full verbatim log + resolution map in internal review log Round 2.

Verdict per path:

• §6.3 wrap — SOUND (cleared for P1 after mechanical fixes). Confirmed: relay cannot learn IK_J; hybrid; deniable. Applied fixes: removed wk_j from the §6.2 transcript (a relay could flip its RFC-7748 top bit → same decoded point/same WK/ct still decrypts, but different octets → SK desync + burned single-use invitation); bound wk_j into the ct AAD; folded kem_ct+KEM-pubkey into the WK info (ML-KEM non-binding hardening); made ss_pq zeroization explicit (§6.4 step 4); generalized the q_reply.srv allowlist check (§6.4 step 2).
• §11.4 session-reset — REDESIGNED (was needs-redesign). The 0.2 one-sided static-authenticated reset failed on every axis — replayable (→ deterministic-nonce reuse = two-time-pad + forgery + permanent DoS), no forward secrecy (no ephemeral×ephemeral term), no KCI resistance (symmetric X25519(IK_A,IK_B)), PQ-downgraded (one message can't carry a mutual ss_pq'), and under-specified (no reset transcript/label → the re-verify SAS might not bind the new keys). ~12 findings retired by one unified redesign: a two-message, mutually-ephemeral, hybrid-PQ, epoch-bound, key-confirmed re-handshake with reset_transcript + ncp1/reset/* labels (§11.4, §13). Added the vaulted-token re-vault invariant (§11.1) and the non-vaulted continuity-secret requirement for silent reset.

Doc/consistency fixes: SAS reconciled to 8 words / 2⁸⁸ everywhere (§4 tiers, §12.5 — the 0.2 change had left stragglers); §13 injectivity reworded to the accurate intra-namespace prefix-free statement; §8 reset envelope framing (keyless 0x01, kind-discriminated); disclosures added for persistent-qid device linkage (§12.9c) and reinstall reset-burst vs duress (§12.9b, §4.7).

Design viability (web-validated, 4 passes): YES. The exact architecture class (no key server, OOB bootstrap, per-direction queues, DR + hybrid PQ) ships in production (SimpleX); @noble is Cure53-audited; react-native-quick-crypto gives native ML-KEM-768 (sub-ms on mobile); 88-bit SAS is conservative. The §6.2 handshake is at/ahead of the 2024-26 literature (it already binds both KEM pubkey and ciphertext into the transcript — the canonical PQXDH mitigation — and is deniability-correct by having no signatures). Two RN landmines are now normative (§14): a CSPRNG health-check gate and native ML-KEM decapsulation.

Confirmed sound, do NOT "fix" into bugs: relay JoinMsg-substitution (relay lacks the invitation ephemerals → collapses to the disclosed OOB-link MITM caught by SAS); the per-channel fresh IK does not block the v2 MLS trust-carry (MLS basic credentials are themselves OOB-verified, directory-free); low-order/all-zero already covered by §2.

New hardening ideas (ranked, with adopt-when) live in internal engineering notes. v1 blockers already folded into this draft; v2 headliners: SPQR-style continuous PQ ratchet (the real remaining PQ gap — §15) and hardware-backed per-channel IK (§15).

Round 3 (draft 0.3 → 0.4) — formal verification in ProVerif

The two new key-agreement paths were machine-checked in ProVerif (symbolic Dolev-Yao model; DH equational theory, KEM as a correct-decapsulation function, HKDF/AEAD as random-oracle/one-way functions). Models + a reproducible Docker harness are committed under the published ProVerif models (ncp-proverif-models.zip); the full write-up with every query result is the formal verification report (published with this spec).

Results (all as intended):

• §6.2 handshake + §6.3 wrap (Verified tier): injective agreement ✅, secrecy of the joiner's identity key IK_J ✅ and ephemeral EK_J ✅ from the relay (the wrap's goal), session-key secrecy ✅, honest run reachable ✅.
• §11.4 reset — mutual injective authentication ✅✅, new-root-key secrecy ✅.
• §11.4 KCI resistance ✅ — with the peer B's own long-term key compromised, B still authenticates A (attacker cannot impersonate a third party to B).
• §11.4 forward secrecy ✅ — the new root key stays secret even after both long-term identity keys leak post-session (the ephemeral×ephemeral term carries it).
• PQ-hybrid ✅✅ — the session key stays secret when the attacker is handed the KEM secret (the classical leg carries) AND when handed all X25519 exponents (the PQ leg carries): confirms harvest-now-decrypt-later resistance.
• Negative control ✅ — the Connected tier (attacker-substitutable invitation, no reverse-scan) correctly FAILS (identity leaks, auth breaks), proving the models find real attacks and the Verified/Connected boundary is load-bearing.

Real gap found & fixed (→ draft 0.4): the draft-0.3 reset used only a one-way (A→B) key confirmation, so ProVerif proved B⟹A injective agreement but REFUTED A⟹B — i.e. A was not authenticated to B, letting an attacker who substitutes reset_resp impersonate B to a reinstalling device. Fixed by adding a mandatory B→A key confirmation (confirm_B in reset_resp, §11.4 step 2/4); with it, ProVerif verifies both-direction injective agreement. This is a genuine protocol correction the manual/LLM-adversarial passes (Rounds 1-2) missed and the formal check caught.

Symbolic-model caveats (documented, not gaps): ProVerif abstracts away computational/encoding issues (e.g. the X25519 top-bit malleability from Round-2 finding #13, and ML-KEM's non-binding property) — those are handled by the transcript/AAD binding fixes and by keeping the security proof robust to a KEM break (the hybrid result). Deniability is argued from the no-signatures design, not re-proven here (would need observational equivalence). A Tamarin cross-check with an explicit MAL-BIND KEM theory remains a nice-to-have but is not a P1 blocker.

Next gate: P1 implementation — the apps’ shared protocol library on the CryptoPrimitives pattern, porting the ProVerif-checked message flows and the DR/PQXDH test vectors.

Round 4 (draft 0.4 → 0.5) — three independent reviews of the v2 product layer

Three fresh-context reviewers (cryptography/protocol, product/UX, engineering feasibility) examined the September design plan, this spec and the mockups. Reports: chat-review-2026-09-18/; consolidation and product team decisions: internal review notes; log: internal review log.

Verdict: §6, §7.1–§7.3 and §11.4 unchanged and still sound. All findings were in the v2 plan's new material; resolved in 0.5 as follows (G0 sign-off blockers marked ★):

• ★ F1 pq_rekey circular/ambiguous → §7.5: header-carried on every message of a chain; root step bound to the chain's dh_pub; sk_e zeroization; epoch rules; KDF_RK_pq. an earlier issue → fixed HDR_CAP, constant hdr_len (§7.2, §8).
• ★ F2 commitment-QR deadlock → form withdrawn (§5.1); raw-byte QR reserved pending S0.
• ★ F3 lease-assisted quiet takeover, F6 no cryptographic teeth / server rollback, F7 move never silent, an earlier issue epoch race → §11.1a approved vs unattended take-over, control:superseded, rotate_otok (§9.2), record_version in the AAD (§11.1), loud alert + Revoke, epoch re-sync in reset_resp (§11.4).
• ★ F4 P9 overstated, an earlier issue K_work not implementable as written, an earlier issue §2.3 rationale → §11.2 K_wrap/K_work/K_store layering, not credential-gated, app-enforced gate, strong mode; P9 and §12.13 rewritten; fixed-slot padded working store.
• ★ F5 OS notification history → content-free default, clear on duress entry, disclosure (§11.3, §12.16). ★ F8 two duress triggers → one session-wide duress state; slot-2 reuse; offline gate (§11.3). an earlier issue PIN storage → keystore-bound verifier, two-slot uniform shape (§11.3).
• F9 per-drive artifact counts → fixed-size ncp-channels container (§11.1). an earlier issue push_mute fingerprint → "Pause notifications" twin, jittered (§9.2, §11.3). an earlier issue backup exclusion (§11.2). an earlier issue per-drive settings off the server (§11.1 record). an earlier issue stale §7.4/§9.2/§11 text updated.
• an earlier issue §15.3 per-app facts, an earlier issue PQ claim → §12.9 corrected; positioning corrected. an earlier issue claim code → peppered HMAC, possession poll_tok, "not a secret from the server", lifecycle with OPENED/BURNED (§5.3, §5.4). an earlier issue deniability → §12.6 content-yes/participation-no.
• Engineering blockers: K_work gating (→ §11.2), iOS notifications (→ queue label, tiers in §9.2), lease enforcement (→ rotate_otok), no native ML-KEM / stale RNG library (→ §14). Also: no separate relay (§9.2), quota as create-rate (§9.1), blob endpoints + inline thumbnail (§10), SQLite working store (§7.4, §11.2), camera/App Links/screen hygiene (§14).
• UX: Connected badge neutral, Check-again amber with disabled composer (§4); mutual SAS, tappable tiles, language-independent word list (§5.5); two-step link-then-code, honest invite states, invitee path (§5.3, §5.3a, §5.4); scan-first entry and terminal screens for the QR ceremony (§5.2).

Not adopted, with reasons: shorter SAS (no commit-reveal round → 88 bits stays, §5.5); leaving the notification shade uncleared on duress entry (the visible name is the worse leak); a separate relay service (server.js already hosts sockets).

an earlier issue formal coverage: Round 5 must model (a) the §7.5 root-step rule across a reordered chain boundary with KEM-break and DH-break experiments, (b) two devices racing a reset (§11.1a), before the pq_rekey flag is enabled in P1.

Next gate: G0 — external human cryptographer's design review of this draft with chat-review-2026-09-18/review-crypto.md alongside, then the Round-5 ProVerif models, then P1.

Round 5 (draft 0.5) — ProVerif: pq_rekey rule and the lease race

Models under ncp-formal/ (ncp-pqrekey*.pv, ncp-lease-race*.pv), report in the formal verification report (published with this spec) Round 5. All intended results obtained: §7.5 root-step agreement and secrecy; post-quantum post-compromise healing with the classical negative control leaking; hybrid (KEM secret leaked); the pending-sk_e caveat confirmed (A5 leaks, as §7.5 states); §11.1a no-fork under an atomic rotate_otok compare-and-swap (B1), race completion witnessed (B2). Modelling note: ProVerif cannot decide inequality-based mutable state, so the lease result is conditional on the server implementing rotate_otok as a single atomic conditional update (Suite 78). Next gate: G0 (external human design review of this draft), then P1.