Signal Protocol Formal Verification
Our Rust implementation of the Signal Protocol undergoes rigorous formal verification to mathematically prove that it correctly implements the protocol and maintains security properties. This documentation explains how we verify the implementation using complementary approaches: ProVerif (symbolic model checking) and Hax with F*, Rocq, or Lean (proof extraction and verification).
What is Formal Verification?
Formal verification is the process of using mathematical techniques to prove that a system behaves correctly. Unlike testing—which can only show that certain inputs produce expected outputs—formal verification can prove that all possible executions satisfy desired properties.
For cryptographic protocols, this means we can prove:
- Key secrecy: Private keys never leak to an attacker
- Forward secrecy: Compromising current keys does not reveal past messages
- Post-compromise security: After a compromise, the protocol "heals" and future messages become secure again
- Authentication: Messages can only be decrypted by the intended recipient
Two Verification Approaches
We use two complementary verification techniques:
ProVerif: Symbolic Model Checking
ProVerif uses a symbolic model (also called the Dolev-Yao model), where cryptographic primitives are treated as abstract operations. The tool automatically explores all possible protocol executions and checks whether an attacker can break security properties.
- Strengths: Handles unbounded sessions, automatic proof search, well-suited for protocol-level properties
- Models: Hand-written ProVerif files that mirror our Rust implementation
- Proves: Key secrecy, forward secrecy, post-compromise security, DH operation order
Hax: Proof Extraction (F*, Rocq, and Lean)
Hax extracts our Rust code into proof-oriented languages: F*, Rocq (formerly Coq), or Lean 4. The extracted code is then verified against security axioms in an abstract cryptography module.
- Strengths: Directly verifies the implementation code, not a separate model
- Process: Rust → Hax extraction → F*/Rocq/Lean code → type checker / rocq compile / lake build
- Proves: Protocol logic correctness, key derivation chains, state transitions
Documentation Overview
| Document | Description |
|---|---|
| Implementation Overview | Dual-crate architecture, X3DH and Double Ratchet flows, what gets verified |
| ProVerif Verification | ProVerif models, what each proves, how to run and interpret results |
| Hax and F* Verification | Extraction pipeline, AbstractCrypto, security axioms, verification workflow |
| Hax and Rocq Verification | Extraction pipeline, AbstractCrypto.v, Rocq verification workflow |
| Hax and Lean Verification | Extraction pipeline, AbstractCrypto.lean, Lake verification workflow |
| Implementation Nuances | HKDF constants, design decisions, known limitations |
Quick Links
- Protocol concepts: See the P2P Signal Protocol documentation for X3DH and Double Ratchet explained in depth
- Security audit: See the Signal Protocol Security Audit for threat model, protocol analysis, and audit findings
- Source code: The signal-protocol repository contains the Rust implementation and formal proof models