Skip to main content

Formal Verification Documentation

Time to read: 15-20 minutes Prerequisites: Basic understanding of Signal Protocol, X3DH, and Double Ratchet Difficulty: Beginner → Intermediate → Advanced progression

Executive Summary​

This documentation presents the formal verification of the Signal Protocol implementation using ProVerif (symbolic model checking) and Hax/F* (Rust-to-F* extraction). We model the protocol's security properties mathematically and prove they hold against powerful attackers.

What You'll Learn​

  • What formal verification is and why it matters for cryptographic protocols
  • All 7 ProVerif models from simple to comprehensive, with complexity ratings
  • Hax and F* verification (Rust extraction, AbstractCrypto, security axioms)
  • Security properties proved (confidentiality, authentication, forward secrecy, etc.)
  • Alignment between formal models and signal-protocol-core with code examples
  • Known limitations of formal verification (what it can/cannot prove)

Quick Reference​

ModelComplexityLinesSecurity PropertiesStatus
x3dh_complete.pvSimple74DH operations, key secrecyVerified
x3dh_security.pvSimple74Authentication, MITM resistanceVerified
x3dh_4dh.pvSimple744 DH operations explainedVerified
double_ratchet_dr.pvMedium87DH ratchet mechanismVerified
double_ratchet_key_derivation.pvMedium93Chain/message key derivationVerified
double_ratchet_security.pvComplex87Forward secrecy, post-compromise securityVerified
signal_protocol_complete.pvComplex73End-to-end propertiesVerified
Hax/F*——Protocol logic, key derivation, stateVerified

Key Findings​

  • All 7 ProVerif models compile successfully and verify their security properties
  • Hax/F*: Rust code extracted to F*, verified against AbstractCrypto axioms
  • Key secrecy proved: Private keys are never accessible to attackers
  • Forward secrecy proved: Compromise of current keys doesn't reveal past messages
  • Post-compromise security proved: System recovers automatically after key compromise
  • Alignment with signal-protocol-core (all DH operations, HKDF constants, AAD format match)

Known limitations: Formal verification assumes ideal cryptography (black-box DH, HKDF), doesn't prove implementation correctness, and doesn't model side-channel resistance. See 07 Known Limitations for details.

Full technical documentation: Signal Protocol Formal Verification

The documentation progresses from beginner-friendly introductions to advanced technical analysis:

Total estimated reading time: ~5 hours for all docs. You can skip ahead based on your interests!

Table of Contents​

Beginner Sections (Start Here)​

  1. 01 Formal Verification Overview

    • What is formal verification?
    • Why use ProVerif for Signal Protocol?
    • Quick introduction to all models
    • Prerequisites and setup

  2. 02 X3DH Formal Proof

    • X3DH models explained (simple, comprehensive demonstration)
    • 4 DH operations formalized
    • Security properties for X3DH proved
    • Beginner-friendly diagrams and math

  3. 03 Double Ratchet Formal Proof

    • Double Ratchet models (key derivation, security proofs)
    • Forward secrecy: how old keys stay secure
    • Post-compromise security: how the system recovers
    • Visual explanations of ratcheting

Intermediate Sections (Deep Dive)​

  1. 04 All ProVerif Models Comprehensive

    • All 7 models with complexity ratings
    • Model-by-model breakdown
    • Query explanations and verification results
    • Code snippets from each model

  2. 05 Security Properties Comprehensive

    • Quick reference table: all properties at a glance
    • Inline explanations in model docs
    • Detailed table of what each property proves
    • Proof summaries with ProVerif queries

Advanced Sections (Technical Implementation)​

  1. 06 Implementation Alignment

    • ProVerif ↔ Rust alignment verification
    • Side-by-side code comparisons
    • HKDF constants alignment table
    • DH operations alignment with line references

  2. 07 Known Limitations

    • What ProVerif can/cannot prove
    • Limitations explained clearly
    • When formal proofs are sufficient vs. need additional analysis

Hax and F* (Technical): For the Hax extraction pipeline, AbstractCrypto, and F* verification, see Technical Formal Verification: Hax and F*.

What You'll Gain​

After reading this documentation, you'll be able to:

  • Understand formal verification and its role in cryptographic security
  • Read and interpret ProVerif models and verification results
  • Explain which security properties are formally proved for Signal Protocol
  • Verify alignment between formal models and Rust implementation
  • Identify limitations of formal verification
  • Decide when formal proofs are sufficient vs. need additional testing

Pre-Reading Checklist​

Before diving in, ensure you understand these concepts:

  • Signal Protocol Basics: X3DH and Double Ratchet concepts
  • Public Key Cryptography: Diffie-Hellman key exchange
  • Symmetric Encryption: AES-256-GCM
  • Key Derivation: HKDF-SHA256
  • Git/GitHub: For following code references

Need a refresher? Check out the Signal Protocol Tutorial sections!

Model Complexity Guide​

Our ProVerif models range from simple demonstration to comprehensive security proofs:

Start with: Simple models if you're new to ProVerif Progress to: Medium models for Double Ratchet mechanics Master: Complex models for comprehensive security proofs

For Different Audiences​

Students Learning Cryptography​

Start with 01 Overview and 02 X3DH. Skip to 05 Security Properties for quick reference. 07 Known Limitations is essential.

Developers Implementing Signal Protocol​

Read 02 X3DH, 03 Double Ratchet, then 06 Implementation Alignment. 04 All Models provides deep implementation insights.

Security Auditors / Researchers​

Start with 04 All Models, then 05 Security Properties, and 07 Known Limitations. 06 Implementation Alignment provides formal correspondence verification.

Getting Started​

Ready to begin? Start with 01 Formal Verification Overview →

Don't forget, the Docusaurus sidebar will show all pages in order, so you can navigate sequentially!

Need Help?​

Document Last Updated: February 2026 Document Version: 1.1 ProVerif Version: 2.05+ Hax/F*: See technical docs Rust Implementation: signal-protocol