ProVerif Verification

We use ProVerif to formally verify our Signal Protocol implementation using symbolic model checking. This document explains what ProVerif is, what each model proves, how to run the proofs, and how to interpret the results.

What is ProVerif?

ProVerif is an automated verification tool for cryptographic protocols. It uses a symbolic model (also called the Dolev-Yao model), where:

• Cryptographic primitives (encryption, hashing, key exchange) are treated as abstract operations with algebraic properties
• The attacker can intercept, modify, and send messages on the network, but cannot break cryptography except through protocol flaws
• The tool explores all possible protocol executions and checks whether security properties hold

This approach is well-suited for protocol-level properties like key secrecy, authentication, and forward secrecy.

Model Hierarchy

ProVerif Models

File	Purpose	What's Proven
x3dh/x3dh_4dh.pv	Demonstrates the 4 X3DH DH operations in isolation	DH operations execute in correct order
x3dh/x3dh_complete.pv	Full X3DH handshake with HKDF constants	Key secrecy, all 4 DH ops, HKDF derivation
x3dh/x3dh_security.pv	Basic X3DH security properties	Key secrecy, authentication events
double_ratchet/double_ratchet_dr.pv	DH ratchet state transitions	Key secrecy, message authentication, state transitions
double_ratchet/double_ratchet_key_derivation.pv	Key derivation chain	Root → chain → message key derivation
double_ratchet/double_ratchet_security.pv	Forward and post-compromise security	Forward secrecy, post-compromise recovery
signal_protocol_complete.pv	Combined X3DH + Double Ratchet	Key secrecy, component correctness

X3DH Models

The X3DH models verify that:

1. DH operations execute in the correct order: $DH_1$, $DH_2$, $DH_3$, $DH_4$ (where $DH_4$ is optional)
2. HKDF derives the shared secret from concatenated DH outputs using the same constants as the Rust implementation
3. Secret keys remain private—the attacker cannot derive them

Double Ratchet Models

The Double Ratchet models verify that:

1. Forward secrecy: Old keys cannot be derived from new keys; compromising the current state does not reveal past message keys
2. Post-compromise security: After a compromise, new messages become secure again (the protocol "heals")
3. Message authentication: Only messages encrypted by the sender can be decrypted by the intended recipient

End-to-End Model Limitation

The signal_protocol_complete.pv model combines X3DH and Double Ratchet but does not link them with a channel. Therefore, full end-to-end correspondence (X3DH handshake → DR state → messages) is not proven. This is a known limitation of the current model.

Implementation Alignment

The ProVerif models are carefully aligned with the Rust implementation:

• X3DH DH operations: Match signal-protocol-core/src/x3dh.rs (DH1–DH4 order)
• HKDF constants: All salts and info strings match formal-proofs/docs/HKDF_CONSTANTS.md
• HKDF signature: ProVerif uses hkdf(salt, ikm, info) to model Rust's Hkdf::new(salt, ikm).expand(info, output) pattern
• AAD format: Matches DH_public_key || message_number || previous_chain_length in double_ratchet.rs

Running the Proofs

Quick Start

cd formal-proofs
./test_proverif.sh

This runs all 7 models. Expected output: 7 compiled, 0 failed, 100% success.

Running Individual Models

# X3DH
proverif proverif/x3dh/x3dh_complete.pv
proverif proverif/x3dh/x3dh_security.pv
proverif proverif/x3dh/x3dh_4dh.pv

# Double Ratchet
proverif proverif/double_ratchet/double_ratchet_dr.pv
proverif proverif/double_ratchet/double_ratchet_key_derivation.pv
proverif proverif/double_ratchet/double_ratchet_security.pv

# End-to-end
proverif proverif/signal_protocol_complete.pv

Docker

docker compose run proverif

Interpreting ProVerif Output

Key Secrecy (Most Important)

RESULT not attacker(sk[]) is true.

This means the attacker cannot derive the secret key. This is the result you want to see—it proves private keys stay private.

Event Queries

RESULT not event(dh1_computed(x)) is false.

When the result is false, it means the event does fire during normal protocol execution. This is expected for events like dh1_computed—they indicate the protocol ran correctly.

Correspondence Queries

RESULT inj-event(encrypt(x)) ==> inj-event(decrypt(x)) is true.

This proves that decryption can only occur if encryption occurred first with the matching key—i.e., authentication holds.

Summary of Expected Results

Query Type	Desired Result	Meaning
not attacker(sk[])	true	Keys are secret
inj-event(A) ==> inj-event(B)	true	Authentication holds
not event(dh1_computed(x))	false	Event fires (normal execution)

ProVerif vs CryptoVerif

We use ProVerif rather than CryptoVerif because ProVerif can model our protocol more faithfully:

Capability	CryptoVerif	ProVerif
X3DH operations	Only 1 DH	All 4 correctly
X3DH operation order	Limited	Matches implementation
Double Ratchet states	Cannot model	Works
Forward secrecy proofs	Cannot	Yes
Post-compromise proofs	Cannot	Yes

Prerequisites

• ProVerif 2.05+: Install via opam install proverif
• OPAM: OCaml package manager; install with sudo apt install opam (Ubuntu/Debian)

See the signal-protocol formal-proofs repository for full installation instructions.