Signal Protocol formal verification

Research, not an audit

These pages are research and development and may not match the live app. Do not treat this as an audit. Shared for testing and demo only. Please use responsibly.

X3DH key agreement and the Double Ratchet, with AES-256-GCM message encryption. Gallery: signal.positive-intentions.com. Source: positive-intentions/signal-protocol. This page reports tests and proofs with the same claim words as ML-KEM (tested / modeled / type-checked / assumed / open). It is not a claim that the Glitr messenger is verified.

Start from the verification report. This page has extract and CI detail.

Interface under test

Callers use identity keys, signed prekeys, one-time prekeys, X3DH, then a Double Ratchet session. Keys are 32-byte X25519 / Ed25519 material. Signatures are 64 bytes. WASM and TypeScript bindings are tested, not extracted.

Production builds enable a crypto backend (X25519, Ed25519, AES-GCM). Extraction builds without that feature so those calls become AbstractCrypto stubs.

Executable tests

Suite	What it covers	Gate
Rust workspace tests	Crypto, keys, X3DH, Double Ratchet, errors	Must pass
Line coverage	Workspace llvm-cov with --ignore-filename-regex 'signal-protocol/src/' so WASM wrappers are not in the denominator. The gate is signal-protocol-core. The only coverage(off) is hkdf_derive_short (HKDF expand of ≤64 bytes).	100% lines
Jest	TypeScript bindings	Must pass
WASM	Node and headless Chrome wasm-pack tests; standalone module load	Must pass
Lint / format	JS Prettier + ESLint (lint:ci). There is no Rust clippy/rustfmt CI job.	Must pass

Typical production cases: key-pair generation, signed prekey verification failure, X3DH with and without a one-time prekey, in-order and out-of-order ratchet messages, AEAD authentication failure.

Symbolic models (ProVerif)

Seven processes. Constants (HKDF salt/info, associated-data layout) are written to match the implementation — that match is intent, not a machine-checked link from ProVerif to Rust. The attacker is the standard Dolev–Yao network. The AEAD equation is idealized (not IND-CCA or nonce-misuse resistance).

Model	What it encodes
Complete X3DH	Four DH operations and implementation HKDF constants
X3DH 4-DH	The four DH steps in isolation
X3DH security	Key secrecy and authentication-related events
Double Ratchet DR	DH ratchet transitions and decrypt correspondence
Key derivation	Root → chain → message keys
Double Ratchet security	Forward secrecy and post-compromise recovery
Combined protocol	X3DH and Double Ratchet as parallel processes

X3DH, as modeled

$$\begin{aligned} \mathrm{DH}_1 &= \mathrm{DH}(\mathit{IK}_A, \mathit{SPK}_B), \\ \mathrm{DH}_2 &= \mathrm{DH}(\mathit{EK}_A, \mathit{IK}_B), \\ \mathrm{DH}_3 &= \mathrm{DH}(\mathit{EK}_A, \mathit{SPK}_B), \\ \mathrm{DH}_4 &= \mathrm{DH}(\mathit{EK}_A, \mathit{OPK}_B), \\ \mathit{SK} &= \mathrm{HKDF}(\mathrm{salt},\; \mathrm{DH}_1 \,\|\, \mathrm{DH}_2 \,\|\, \mathrm{DH}_3 \,\|\, \mathrm{DH}_4,\; \mathrm{info}). \end{aligned}$$

$\mathit{OPK}_B$ is omitted when Bob has no one-time prekey; the 4-DH model still checks the four-share case.

Double Ratchet, as modeled

A sending chain produces one-time message keys. After a DH ratchet step the old chain is discarded:

$$k_{\mathrm{msg}}^{(n)} = \mathrm{KDF}_{\mathrm{chain}}(\mathit{CK}_n), \qquad \mathit{CK}_{n+1} = \mathrm{KDF}_{\mathrm{chain}}'(\mathit{CK}_n).$$

Forward secrecy (modeled): from a later chain key, the attacker cannot derive an earlier $k_{\mathrm{msg}}$. Post-compromise (modeled): after an injected compromise event, later honest messages can still be produced. Neither query is a proof about X25519.

Associated data matches the implementation layout

$$\mathrm{AAD} = \mathit{DH}_{\mathrm{pub}} \,\|\, n \,\|\, \mathit{pn}$$

(public DH key, message number, previous chain length).

Query results

Property	Status	Notes
Key secrecy	Modeled	Query-specific per model; the combined model is parallel and unlinked
Four DH operations execute in order	Modeled	Complete and 4-DH models
Forward secrecy of old message keys	Modeled	Security model (old_key_not_reachable_from_new)
Recovery after compromise	Modeled	Same model
Decrypt implies a prior encrypt	Modeled	DR and key-derivation models
End-to-end correspondence (handshake → first ratchet → messages)	Open	Combined model: processes are not linked by a channel
Alice/Bob authentication correspondence on full X3DH	Open	Same linking-channel limit

A local “7/7 compiled” run means every model parsed and the stated queries were discharged. It is not the same sentence as “the messenger is verified”.

Extracted Rust (hax → F*, Rocq, Lean)

Hand-written AbstractCrypto modules assume (they do not prove) the usual group and signature facts:

$$\begin{aligned} \mathrm{DH}(a, \mathrm{pub}(b)) &= \mathrm{DH}(b, \mathrm{pub}(a)), \\ \mathrm{Verify}(\mathrm{pub}(a),\; \mathrm{Sign}(a, m),\; m) &= \mathsf{true}, \\ a \neq a' &\implies \mathrm{Verify}(\mathrm{pub}(a),\; \mathrm{Sign}(a', m),\; m) = \mathsf{false}, \\ \mathrm{Dec}(k, \mathrm{Enc}(k, m, \mathit{aad}, n)) &= m. \end{aligned}$$

They also assume injectivity of $\mathrm{pub}(\cdot)$ and that compromising a long-term key does not identify a distinct ephemeral DH secret. Those are axioms for the glue, not theorems about the production backend.

Listed targets for X3DH (authentication, forward secrecy, indistinguishability, mutual agreement) and the Double Ratchet (message-key uniqueness, forward secrecy after compromise, chain integrity, out-of-order handling) are goals. There is no finished proof script that the extracted Double Ratchet satisfies them.

Rocq post-processes some Double Ratchet internals into Axiom stubs where the ? / ControlFlow encoding does not type-check. That is type-checking with holes.

What CI type-checks

Backend	Automated job	Depth
F*	Lite extract	Extracted modules except Double Ratchet
Rocq	Abstract only	AbstractCrypto
Lean	Lite	AbstractCrypto

A full extract (including Double Ratchet) exists as a local target. It is not the default CI job.

Toolchain

Tool	Pin used for verification images
OCaml / opam	5.1.1
Z3 (F*)	4.13.3
Lean	4.28.1
Workspace Rust	1.85
hax-lib crate	0.3

F* and Rocq come from opam without a finer version pin. hax itself is cloned at image build time.

What this does not prove

• The production crypto backend refines AbstractCrypto
• X25519, Ed25519, HKDF, or AES-GCM themselves
• WASM / JS bindings (they are tested, not extracted)
• A single session that feeds X3DH’s $\mathit{SK}$ into Double Ratchet initialization
• The Glitr messenger, PQXDH, or the recipient cascade

Next: ML-KEM — hybrid wrapper and the pinned libcrux suite.