PQXDH 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.

pqxdh composes X25519, ML-KEM-1024, HKDF, an initial AEAD, and a Double Ratchet hook toward Signal PQXDH revision 3. Gallery: positive-intentions.github.io/pqxdh. This page uses the same claim words as Signal Protocol and ML-KEM (tested / modeled / type-checked / assumed / open / cited). It is not an audit of the messenger.

Start from the verification report.

Interface under test

Primitives stay in siblings. This crate owns the composition:

$$\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)\ \text{(optional)}, \\ (\mathit{ct}, \mathit{ss}) &= \mathrm{Encaps}(\mathit{PQPK}_B), \\ \mathit{SK} &= \mathrm{HKDF}(0^{32},\; F \,\|\, \mathrm{DH}_{1..n} \,\|\, \mathit{ss},\; \texttt{PQXDH-v1\_CURVE25519\_SHA-256\_ML-KEM-1024}), \\ \mathrm{AD} &= \mathrm{EncodeEC}(\mathit{IK}_A) \,\|\, \mathrm{EncodeEC}(\mathit{IK}_B). \end{aligned}$$

Documented deviations stay in every status table: Ed25519 is not XEdDSA; HKDF is SHA-256 only; encodings are not libsignal protobufs.

Production enables crypto-backend (path deps on signal-protocol-core and ml-kem-core). Extraction builds --no-default-features. Stubs use AbstractPqxdh axioms.

Executable tests

Suite	What it covers	Gate
Rust tests (backend on)	Keygen, bundle verify, initiate/respond, optional OTPK, initial AEAD abort, handshake→session (handshake_session.rs and session.rs)	Must pass
Rust tests (backend off)	Length and field-rejection paths on extractable stubs	Must pass
Line coverage	pqxdh-core	100% lines on both feature builds
proptest	Encode/decode inverses, derive_sk sensitivity, honest handshake, tampered SPK	Must pass
Implementation KATs	Fixed-seed replay (npm run kats:gen). Not official Signal vectors	Must pass
Fuzz	decode_ec, decode_kem, verify_prekey_bundle, respond	Time-boxed CI
WASM	Handshake + session APIs, including one-time vs last-resort PQ prekeys	Must pass

Wrapper lemmas

Hand-written AbstractPqxdh (F*, Rocq, Lean).

Assumed

Assumption	Formal content
DH commutativity	$\mathrm{DH}(a, \mathrm{pub}(b)) = \mathrm{DH}(b, \mathrm{pub}(a))$
KEM correctness	Cited from ML-KEM / libcrux
HKDF / AES-GCM / Ed25519	Sibling and crate axioms
Double Ratchet init	Cited from Signal Protocol

Proved on the spec (glue)

Wrong-length keys fail before DH/KEM/HKDF. KDF IKM length is $32 + 32\cdot n + 32$ for $n \in \{3,4\}$. AD is two EncodeEC values. session_from_handshake rejects $\lvert \mathit{SK} \rvert \neq 32$.

Symbolic models (ProVerif)

Model	Queries
pqxdh_kdf.pv	IKM = $F \|\| \mathrm{DH}_{1..n} \|\| \mathit{ss}$; SK secrecy
pqxdh_4dh_kem.pv	Four DH ops + encaps/decaps
pqxdh_handshake.pv	initiate/respond, optional OTPK, initial AEAD abort
pqxdh_security.pv	Forged SPK/PQ signatures do not yield an honest SK (Modeled (honest bundle only))
pqxdh_hybrid_binding.pv	SK secret if only DH or only KEM is given to the attacker
pqxdh_session.pv	Private channel c_sk from handshake to ratchet; session_decrypt(m) \Rightarrow handshake_agree(sk)
pqxdh_complete.pv	Bundle → handshake → c_sk → first ratchet messages

Session and complete models are one Alice process and one Bob process that output SK on a private channel, then continue as ratchet processes that read that same SK. That is the linking gap left open in signal-protocol’s combined model.

These assume DH, KEM, HKDF, and AEAD equations. They do not prove X25519, libcrux, or AES-GCM. Constants match the Rust by intent.

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

Backend	Automated job	Depth
F*	Full stub extract	Type-checks extracted pqxdh-core plus AbstractPqxdh
Rocq	Extract + length lemmas	? bodies may be axiomatized
Lean	AbstractPqxdh only	Extracted Lean is not built in this job

There is no verify-libcrux job here. Lattice math stays on the ml-kem pin.

Automated jobs

Job	What it runs
Format, Clippy, cargo test	Production and stub pqxdh-core
Coverage	100% lines on both feature builds
WASM	Node wasm-pack
ProVerif	Seven models
F* / Rocq / Lean	Stub extract and axiom modules
Fuzz	Time-boxed cargo-fuzz

verify:host:full is ProVerif + F* + Rocq + Lean.

What this does not prove

• WASM bindings or the gallery
• X25519, Ed25519, HKDF, AES-GCM, or libcrux lattice math
• libsignal wire compatibility (not claimed)
• Official Signal PQXDH KATs (they are not published)
• The recipient cascade, git mailbox delivery, or a stolen device
• The Glitr messenger
• Refinement from the crypto-backend production build to AbstractPqxdh

Next: crypto formal verification — password sealing and the modeled cascade composition.