Formal Verification Overview

Time to read: 30 minutes
Prerequisites: None (we'll build from scratch)
Difficulty: Beginner
Next: 02 X3DH Formal Proof

The Simple Story

Imagine you're building a cryptographic protocol (like Signal). How do you know it's actually secure?

You could:

Test it (but tests don't prove security)
Review code manually (humans make mistakes)
Use formal verification (mathematical proof of security properties)

Formal verification means: We use mathematics to prove that no attacker (no matter how powerful) can break the security properties we care about.

Think of it like: Instead of testing a lock to see if it opens, we mathematically prove that there's no way to pick it!

Mental Model: What is Formal Verification?

Hold this picture in your head:

The Process:

Model the protocol as a mathematical object (using ProVerif syntax)
Specify what security property you want to prove
Run the ProVerif verifier (automated tool)
Get a mathematical answer: PROVED or FALSE (with proof/counterexample)

Why use ProVerif?

It's a widely-used, academically-verified tool
It's designed specifically for cryptographic protocols
It's automatic (you don't write the proof manually, the tool does it)
It handles attacker capabilities, secrecy, authentication, etc.

The Story: Why We Need Formal Verification

Eve (our attacker) claims: "I can break Signal Protocol!"

Alice and Bob say: "Prove it!"

Eve tries:

Message tampering (fails - signatures)
Key compromise (fails - forward secrecy)
Replay attacks (fails - nonces)
...and many more attempts

But how do Alice and Bob KNOW Eve can't find a new attack?

Answer: Formal verification!

Instead of listing every possible attack (impossible!), we:

Model the Signal Protocol mathematically
Define what "secure" means (no attacker can learn secrets, etc.)
Prove: For ALL possible attackers, with ANY capabilities, the security holds

Theorem: "For any attacker, all secrets remain confidential" ← This is what we prove!

The Mathematics

What Does ProVerif Verify?

ProVerif proves (or disproves) reachability queries:

\text{not attacker}(s) \quad \text{"Secret } s \text{ is never reachable by attacker"}

\text{inj-event}(a) \implies \text{inj-event}(b) \quad \text{"If event } a \text{ happens, then } b \text{ must also happen"}

Key Query Types:

Secrecy: Can the attacker learn a secret?
Authenticity: If Alice sends a message, did Bob receive it?
Correspondence: Can we prove that events happen in a specific order?

Simple X3DH Example

In X3DH, we prove:

\forall x: \text{bitstring}; \quad \text{not attacker}(\text{shared_secret}[x])

Read aloud: "For all possible shared secrets, the attacker can never learn them."

What this proves:

Even if Eve intercepts all messages
Even if Eve knows all public keys
Even if Eve knows all past session keys
Eve still can't derive the current shared secret

Double Ratchet Forward Secrecy Example

In Double Ratchet, we prove:

\text{inj-event}(\text{encrypt}(m_n)) \implies \text{not attacker}(\text{key}_x) \quad \text{for } x < n

Read aloud: "If we encrypt message number $n$ , then all previous keys (with index $< n$ ) are unreachable to the attacker."

What this proves:

If Eve compromises the current key
She can ONLY decrypt the current message
She CANNOT decrypt any previous messages
This is forward secrecy

See It Happen: ProVerif Verification

Let's watch ProVerif verify a security property:

The Magic: ProVerif searches ALL possible attack scenarios (including ones you never thought of) and tells you if the property holds!

Why ProVerif for Signal Protocol?

What ProVerif Does Well

Cryptographic protocols: Perfect for key exchange, ratcheting, handshakes
Automatic: No manual proof writing - the tool does it
Attacker modeling: Built-in powerful attacker (Dolev-Yao)
Composability: Can model complex protocols layer by layer

What ProVerif Cannot Do

Implementation verification (does the code correctly implement the model?)
Side-channel resistance (timing attacks, cache attacks)
Computational hardness assumptions (we assume ECC is hard)
Hardware/firmware security (out of scope)

Result: ProVerif proves the protocol design is secure, but we still need code review and testing for the implementation.

Beyond ProVerif: The signal-protocol implementation also uses Hax/F* (Rust-to-F* extraction) to verify protocol logic and key derivation against AbstractCrypto axioms. See the Technical Formal Verification docs for details.

The 7 ProVerif Models

We've created 7 ProVerif models for the Signal Protocol, ranging from simple demonstrations to comprehensive security proofs:

Simple Models (Beginner-Friendly)

1. x3dh_complete.pv

Purpose: Simple X3DH model with all 4 DH operations
Complexity: Simple (74 lines)
What it proves: DH operations correct, keys derived correctly
Good for: Understanding X3DH in ProVerif

2. x3dh_security.pv

Purpose: Authentication and MITM resistance
Complexity: Simple (74 lines)
What it proves: Attacker can't forge signatures, MITM attacks fail
Good for: Understanding authentication formalization

3. x3dh_4dh.pv

Purpose: Explicit demonstration of 4 DH sequence
Complexity: Simple (74 lines)
What it proves: DH1 → DH2 → DH3 → DH4 (order correct)
Good for: Understanding the 4 DH operations

Medium Models (Next Level)

4. double_ratchet_dr.pv

Purpose: Double Ratchet DH ratchet mechanism
Complexity: Medium (87 lines)
What it proves: DH ratchet steps, root key updates
Good for: Understanding Double Ratchet mechanics

5. double_ratchet_key_derivation.pv

Purpose: Chain key → message key derivation
Complexity: Medium (93 lines)
What it proves: HKDF chain works, AAD format correct
Good for: Understanding key derivation in Signal

Complex Models (Advanced)

6. double_ratchet_security.pv

Purpose: Comprehensive security proofs
Complexity: Complex (87 lines)
What it proves:
- Forward secrecy (previous keys unreachable)
- Post-compromise security (system recovers)
- Message authentication (encrypt → decrypt correspondence)
Good for: Understanding the full Double Ratchet security

7. signal_protocol_complete.pv

Purpose: End-to-end protocol model
Complexity: Complex (73 lines)
What it proves: Combined X3DH + Double Ratchet properties
Good for: Understanding the complete protocol

See: 04 All ProVerif Models for full details on all models.

Quick Check

What is formal verification?

Mathematical proof of security properties

We model the protocol as a mathematical object, specify security properties, and use ProVerif to prove (or disprove) that no attacker can violate them.

Why use ProVerif for Signal Protocol?

Automated cryptographic protocol verifier

ProVerif is designed to handle Diffie-Hellman, public key encryption, signatures, and other crypto operations. It automatically proves security properties without manual proof writing, handling the full search space of possible attacks.

What can ProVerif prove?

Secrecy, authentication, correspondence properties

ProVerif can prove:

Secrets remain confidential (not reachable by attacker)
Events happen in specific order (correspondence)
Authentication holds (can't forge signatures)

It CANNOT prove:

Implementations are correct (code bugs)
Side-channel resistance (timing attacks)
Computational hardness (assumes primitives are secure)

What can't ProVerif prove?

Implementation correctness, side-channel resistance

ProVerif assumes:

Cryptographic primitives work perfectly (black box model)
No timing variations, no side channels
Computational problems are mathematically hard (ECC, discrete log)

We need:

Code review → implementation verification
Fuzzing/pentesting → side-channel analysis
Cryptographic research → hardness assumptions

See 07 Known Limitations for details.

What We're Modeling

X3DH: The Handshake

Real Protocol (Alice → Bob):

Alice downloads Bob's public keys (IK, SPK, OPK)
Alice generates ephemeral key (EK_A)
Alice computes 4 DH operations:
- DH1 = DH(IK_A, SPK_B)
- DH2 = DH(EK_A, IK_B)
- DH3 = DH(EK_A, SPK_B)
- DH4 = DH(EK_A, OPK_B) (if OPK exists)
Alice derives shared secret: $S = \text{HKDF}(DH_1 \| DH_2 \| DH_3 \| DH_4)$
Alice sends message encrypted with keys from S

ProVerif Model (x3dh_complete.pv):

(* DH1 = DH(Identity_Alice, SignedPreKey_Bob) *)
let dh1 = compute_dh(identity_a, signed_prekey_b_pub) in

(* DH2 = DH(Ephemeral_Alice, Identity_Bob) *)
let dh2 = compute_dh(ephemeral_a, identity_b_pub) in

(* DH3 = DH(Ephemeral_Alice, SignedPreKey_Bob) *)
let dh3 = compute_dh(ephemeral_a, signed_prekey_b_pub) in

(* DH4 = DH(Ephemeral_Alice, OneTimePreKey_Bob) *)
let dh4 = compute_dh(ephemeral_a, one_time_prekey_b_pub) in

(* Combine all 4 DH outputs *)
let combined = concat(dh1, concat(dh2, concat(dh3, dh4))) in

(* Derive root key from combined DH outputs *)
let root = hkdf(hkdf_salt_x3dh(), combined, hkdf_info_x3dh()) in

Proved: The attacker can never derive the root key from public information alone.

Double Ratchet: Per-Message Keys

Real Protocol (Double Ratchet steps):

DH Ratchet: New DH pair every $\approx$ n messages
Symmetric Ratchet: New chain key every message
Chain Key → Message Key: HKDF each time
Chain Key Advancement: New chain key for next message

ProVerif Model (double_ratchet_key_derivation.pv):

(* Compute DH output from new DH pair *)
let dh_out = dh(ik_a, dh_public_key) in

(* Derive new root key from DH output *)
let root_new = hkdf(salt_dh_ratchet, dh_out, hkdf_info_chain_key()) in

(* Derive chain key from root key *)
let chain_new = hkdf(hkdf_info_chain_key(), root_new, hkdf_info_chain_key()) in

(* Derive message key from chain key *)
let msg_key = hkdf(info_msg, chain_new, info_msg) in

(* Format AAD for message authentication *)
let aad = aad_format(dh_public_key, message_number, previous_chain_length) in

Proved:

Message keys are never exposed to attacker
Chain keys are never exposed to attacker
AAD format matches implementation

Why We Care

The Problem: How Do We Know It's Secure?

Traditional approaches:

Testing: Finds bugs, but can't prove security
Code Review: Catches issues, but humans miss edge cases
Penetration Testing: Finds vulnerabilities, but not exhaustive

The Solution: Formal Verification

\text{Protocol } P \text{ is "Formally Verified" } \iff \forall \text{ attacker } \mathcal{A}, \text{ property } \Pi \text{ always holds}

For Signal Protocol:

$\Pi_1$ : No attacker can learn shared secrets (secrecy)
$\Pi_2$ : No MITM possible (authentication)
$\Pi_3$ : Past keys stay secure after compromise (forward secrecy)
$\Pi_4$ : System recovers after compromise (post-compromise security)

Result: Mathematical guarantees that the protocol is secure.

Caveat: Not a Silver Bullet

Formal verification proves the protocol design is secure, but:

Implementation bugs can still exist (use code review + testing)
Side-channel attacks possible (use timing analysis + platform hardening)
Computational assumptions: We assume ECC is hard (need cryptographic research)

Best Approach: Combine formal verification ( protocol) + code review ( implementation) + testing ( runtime) + security audit ( holistic).

Key Takeaways

Formal verification = Mathematical proof of security properties
ProVerif = Automated tool for cryptographic protocols
Secrecy queries = Prove secrets never reach attacker
Correspondence queries = Prove events happen in order
7 models = From simple demos to comprehensive proofs
X3DH model = 4 DH operations formally verified
Double Ratchet model = Forward secrecy + post-compromise security proved
Limitation = Protocol secure ≠ implementation secure

Next Steps

Now that you understand what formal verification is, let's see it applied to X3DH:

Continue: 02 X3DH Formal Proof

We'll explore:

How X3DH is modeled in ProVerif
What security properties are proved
How the 4 DH operations work mathematically
Beginner-friendly diagrams and explanations

The Simple Story​

Mental Model: What is Formal Verification?​

The Story: Why We Need Formal Verification​

The Mathematics​

What Does ProVerif Verify?​

Simple X3DH Example​

Double Ratchet Forward Secrecy Example​

See It Happen: ProVerif Verification​

Why ProVerif for Signal Protocol?​

What ProVerif Does Well​

What ProVerif Cannot Do​

The 7 ProVerif Models​

Simple Models (Beginner-Friendly)​

Medium Models (Next Level)​

Complex Models (Advanced)​

Quick Check​

What We're Modeling​

X3DH: The Handshake​

Double Ratchet: Per-Message Keys​

Why We Care​

The Problem: How Do We Know It's Secure?​

The Solution: Formal Verification​

Caveat: Not a Silver Bullet​

Key Takeaways​

Next Steps​

Further Reading​