Known Limitations of Formal Verification

Time to read: 35 minutes
Prerequisites: Understanding of all formal verification docs
Difficulty: Advanced
Related: Signal Protocol Security Audit

---

The Simple Story

Formal verification is powerful but not magic.

What It Proves:

• Protocol design is mathematically sound
• No logical flaws in the model
• No attacker can violate specified security properties

What It Does NOT Prove:

• Implementation correctness
• Side-channel resistance
• Computational hardness assumptions
• Real-world performance issues

This document explains these limitations clearly so you understand what's proven and what's NOT proven.

---

Mental Model: Proven vs. Assumed

Hold this picture in your head:

---

Limitation Summary

Category	Limitation	What It Means	How to Address
Implementation	ProVerif proves MODEL secure, not CODE correct	Bugs in code can happen even with secure protocol	Code review + testing + fuzzing
Side-Channels	Assumes no timing/cache variations	Real platforms have timing attacks	Timing analysis + platform hardening
Hardness	Assumes ECC, discrete log are hard	If these break, protocol breaks	Follow crypto research + post-quantum crypto
Performance	Doesn't model performance/memory	Real-world resource constraints	Performance testing + load testing
Black-Box Cryptography	Assumes crypto primitives work	If X25519 has bugs, flaws propagate	Use audited crypto libraries
Network Reality	Models network as black-box	Real-world: packet loss, DoS, etc.	Network testing + resilience design
Human Factors	Assumes parties follow protocol	Users can be tricked, keys mishandled	User education + operational security
Quantum Future	No quantum resistance proven	Quantum computers could break ECC	Plan for post-quantum migration
End-to-End Correspondence	X3DH ↔ DR not linked in ProVerif	signal_protocol_complete.pv doesn't channel-link	See implementation nuances
Double Ratchet F*	F* verification resource-intensive	verify-lite skips DR; full verify needs 512MB	Use make verify-lite for iteration

---

Limitation 1: Implementation Correctness

WARNING: Formal Verification ≠ Code Verification

What ProVerif Proves:

• The mathematical MODEL of the protocol is secure
• All attacker models cannot break the protocol

What It Does NOT Prove:

• The IMPLEMENTATION matches the MODEL
• The code has no bugs
• The code is compiled correctly

Why This Matters

Example Scenarios:

Scenario A: Code Bug

• ProVerif says: Protocol is secure
• Implementation: Off-by-one error in array index
• Result: Buffer overflow, memory corruption
• Formal verification: Doesn't catch implementation bugs

Scenario B: Mismatch

• ProVerif says: DH1 = DH(IK_A, SPK_B)
• Implementation: Swaps to DH(SP_B, IK_A) due to copy-paste error
• Result: Wrong DH computation
• Formal verification: Doesn't verify code-model correspondence

The Solution

Formal Verification + Implementation Verification:

Best Practices:

• Formal verification proves protocol design secure
• Code review verifies implementation matches model
• Testing confirms edge cases work
• Fuzzing catches implementation bugs
• Together: Protocol + Implementation both verified

Addressing This Limitation

We Addressed It:

• Document 06 Implementation Alignment proves ProVerif ↔ Rust match
• Line-by-line comparisons verify code-model correspondence
• GitHub links provided for verification

You Should Also:

• Add unit tests for all protocol operations
• Add integration tests for X3DH and Double Ratchet
• Use fuzzing tools (AFL, libFuzzer) on crypto code
• Conduct code reviews before merging
• Use Rust's memory safety to prevent buffer overflows

---

Limitation 2: Side-Channel Resistance

WARNING: ProVerif Doesn't Model Timing, Cache, Power

What ProVerif Assumes:

• All operations take the same time
• No cache-based information leakage
• No power analysis possible
• Cryptographic operations are black-boxes

Reality:

Timing Attacks:

// DANGEROUS: Not constant-time
fn compare_keys(a: &[u8], b: &[u8]) -> bool {
    for i in 0..a.len() {
        if a[i] != b[i] {
            return false; // Early exit leaks info!
        }
    }
    true
}

Result: Attacker measures time to learn where keys differ.

Constant-Time Version:

// SAFE: Constant-time comparison
fn compare_keys(a: &[u8], b: &[u8]) -> bool {
    let mut result = 0u8;
    for i in 0..a.len() {
        result |= a[i] ^ b[i]; // Always processes all bytes
    }
    result == 0
}

ProVerif: Doesn't model timing difference between these two versions.

How to Address

Platform-Specific Hardening:

• Use constant-time library functions (subtle crate in Rust)
• Avoid early returns in key comparisons
• Use hardware acceleration (AES-NI) when available
• Compile with anti-timing-attack flags
• Test timing variations manually

For This Project:

// Use the `subtle` crate for constant-time operations
use subtle::ConstantTimeEq;

impl ConstantTimeEq for [u8; 32] {
    fn ct_eq(&self, other: &Self) -> subtle::Choice {
        let mut result = subtle::Choice::from(1u8);
        for i in 0..32 {
            result &= self[i].ct_eq(&other[i]); // Constant-time
        }
        result
    }
}

WARNING: JavaScript/WebAssembly Side-Channels

WASM in Browser:

• JavaScript timing can leak information even in WASM
• Browser cache can expose patterns
• Resource contention (multitab browser) causes timing variations

Mitigation:

• Minimize timing-critical operations in JavaScript
• Add random delays to blur timing
• Use browser security APIs (when available)

---

Limitation 3: Computational Hardness Assumptions

WARNING: ProVerif Assumes Crypto Primitives Are Unbreakable

ProVerif Assumptions:

• DH operation is perfectly secure
• Digital signatures are unforgeable
• Symmetric encryption is indistinguishable
• Hash functions are collision-resistant

If These Fail, All Proofs Fail:

Example: Quantum Computers

• Proverif says: DH(EK_A, IK_B) is secure
• Quantum: Shor's algorithm breaks ECC
• Result: Signal Protocol compromised

Current Cryptographic Landscape

What We Assume:

• X25519 ECDH has 128-bit security
• Ed25519 signatures are unforgeable
• AES-256-GCM is secure
• SHA-256 is collision-resistant

Evidence:

• Decades of research (2000s-2020s)
• NIST/FIPS standardization
• Extensive cryptanalysis
• No practical breaks found

But NOT Guaranteed:

• Future research could break these
• Quantum computers (if practical) would break ECC
• Side-channel attacks can break implementations

How to Address

Monitor Crypto Research:

• Follow NIST/Cryptology news
• Update cryptographic primitives if broken
• Plan for post-quantum migration
• Use hybrid approaches (classical + post-quantum)

For This Project:

• Consider adding ML-KEM or other post-quantum KEM as an option
• Follow CVEs for dependencies:
  • curve25519-dalek (ECC library)
  • ed25519-dalek (signatures)
  • aes-gcm (encryption)
  • sha2 (hashing)

---

Limitation 4: Black-Box Cryptography Model

WARNING: ProVerif Assumes Crypto Primitives Work Correctly

ProVerif Models:

fun dh(skey, pkey): bitstring.
fun sign(message, skey): signature.
fun encrypt(key, message): ciphertext.

let dh_out = dh(private_key, public_key) in
let sig = sign(message, private_key) in
let cipher = encrypt(key, message) in

ProVerif:

• Treats dh(), sign(), encrypt() as perfect mathematical functions
• No bugs in implementation (assumes)
• No timing variations (assumes)
• Implementation is unbreakable (assumes)

Reality:

• If curve25519-dalek has a bug, the protocol fails
• If ed25519-dalek has a timing leak, signatures are forgeable
• If aes-gcm has side-channel vulnerability, encryption is weak

How to Address

Use Well-Audited Libraries:

• curve25519-dalek (peer-reviewed Rust crate)
• ed25519-dalek (peer-reviewed Rust crate)
• aes-gcm (AES-NI hardware accelerated)
• sha2 (well-studied hash function)

Monitor Vulnerabilities:

# Check for CVEs
cargo audit
cargo outdated

# Follow dependency updates
cargo update

Use Dependency Scanning:

• GitHub Dependabot
• RenovateBot
• Cargo Audit
• Snyk

---

Limitation 5: Network Reality Model

WARNING: ProVerif Doesn't Model Network Conditions

ProVerif Model:

free c: channel [private].

out(c, message).    // Send
in(c, message).    // Receive (instantly!)

Assumes:

• Network delivers messages perfectly
• No packet loss
• No reordering
• No delay variations
• No DoS attacks

Reality:

• Packet loss causes message delivery failures
• Reordering makes message sequencing tricky
• Delays cause timeout errors
• DoS attacks prevent communication
• Network partitions break the protocol

How This Affects Security

DoS Vulnerability:

ProVerif says: Attacker cannot learn secrets 
But if attacker can:
- Block network traffic (DoS)
- Exhaust resources (message flood)
- Cause timeouts
Result: Communication disrupted

Protocol is secure, but unavailable

Remediation:

• Add rate limiting (prevent message flooding)
• Add retry logic (handle packet loss)
• Add timeout handling (resilience)
• Add DoS detection and blocking

Example: Flood Attack

Scenario:

// VULNERABLE: No rate limiting
async fn handle_message(message: Message) {
    // Process EVERY message
    let decrypted = decrypt(&message)?;
    process(decrypted)?;
}

// DoS: Send 10,000 messages per second → Server crashes

Fixed:

// SECURE: With rate limiting
async fn handle_message(message: Message) {
    if rate_limiter.check_limit() {
        return Err("Too many messages");
    }

    let decrypted = decrypt(&message)?;
    process(decrypted)?;
}

Formal verification: Doesn't model DoS resilience (implementation requirement).

---

Limitation 6: Human Factors

WARNING: ProVerif Assumes Parties Follow Protocol

ProVerif Models:

• Alice follows the protocol correctly
• Bob follows the protocol correctly
• No one makes mistakes

Reality:

User Mistakes:

• User copies private keys unencrypted
• User shares public keys over untrusted channels
• User doesn't verify signatures
• User stores secrets in weak passwords

Example:

Correct Use:

// Store encrypted
let encrypted = encrypt_aes_gcm_key_derivation(user_password, private_key)?;
fs::write("private.key.enc", encrypted)?;

Mistake:

// Store plaintext!
fs::write("private.key", private_key)?;  //  DANGEROUS

Formal verification: Doesn't model user behavior, only protocol correctness.

How to Address

User Education:

• Don't share private keys
• Use strong passwords
• Verify peer identities
• Keep software updated

Built-in Protection:

• Enforce key encryption at rest
• Verify channel integrity
• Warn before sending unencrypted
• Auto-delete sensitive data

---

Limitation 7: Quantitative Performance

WARNING: ProVerif Doesn't Measure Performance

ProVerif Model:

• Operations take one step (abstract)
• No memory usage
• No time limits
• No resource constraints

Reality:

Performance Problems:

ProVerif says: Derive 10,000 keys 
Reality: Takes 5 seconds, 100 MB memory

ProVerif says: X3DH works 
Reality: Takes 50 ms, 2 MB memory

For Real-World Use:

• Mobile devices have limited memory
• Browser WASM has performance limits
• Network bandwidth affects responsiveness

How to Address

Performance Testing:

#[bench]
fn bench_x3dh_handshake() {
    let start = Instant::now();
    x3dh_handshake(alice_keys, bob_keys)?;
    let elapsed = start.elapsed();
    assert!(elapsed < Duration::from_millis(50));  // < 50ms

    // Memory usage: < 1MB
    let memory = get_memory_usage();
    assert!(memory < 1024 * 1024);
}

Monitoring:

• Track message encryption time
• Track memory usage
• Track network latency impact
• Set performance thresholds

---

Critical Limitation: No End-to-End Channel Linking

IMPORTANT: signal_protocol_complete.pv Limitation

From 03 Double Ratchet Formal Proof:

"Note: The signal_protocol_complete.pv model doesn't link the X3DH handshake to the Double Ratchet phase with a channel, so it doesn't prove the full end-to-end correspondence."

What This Means:

What ProVerif Proves:

• X3DH handshake is secure (separate model)
• Double Ratchet messaging is secure (separate model)

What ProVerif Does NOT Prove:

• X3DH handshake leads to correct Double Ratchet initialization
• End-to-end message delivery from Alice → Bob

Why This Is Important:

Formal verification models X3DH and Double Ratchet separately. The complete model doesn't link them via a channel (e.g., in(c, handshake) → out(c, double_ratchet_start)). Therefore:

• Cannot prove: "If Alice does X3DH, then Double Ratchet starts with the correct root key"
• Cannot prove: "If handshake fails, Double Ratchet doesn't start"

What This Means:

• Individual phases are formally verified
• End-to-end connection relies on implementation correctness
• Integration testing is required

---

Quick Check: What ProVerif Proves vs. What It Doesn't

ProVerif Proves:

Protocol design is mathematically sound

X3DH handshake is secure Double Ratchet provides forward secrecy No logical flaws in protocol Attacker cannot break the model

ProVerif Does NOT Prove:

Everything else: implementation, side-channels, hardness, etc.

ProVerif does NOT prove:

• Implementation is correct (code bugs possible)
• Side-channel resistance (timing attacks possible)
• Cryptographic primitives are secure (if library has bugs)
• Network resilience (packet loss, DoS)
• User behavior follows protocol (human mistakes)
• Performance requirements (speed, memory)
• Quantum resistance (future computers)
• End-to-end correspondence (X3DH → Double Ratchet link)

---

Key Takeaways

Proven: Protocol design is mathematically secure
Proven: 7 security properties hold for all attackers
Proven: ProVerif ↔ Rust implementation aligned

Not Proven: Implementation is correct
Not Proven: Side-channel resistance
Not Proven: Computational hardness assumptions hold forever
Not Proven: End-to-end X3DH → Double Ratchet linking

The Complete Security Picture

Result: Formal verification is ONE piece of the security puzzle. Alone, it proves protocol security. With other practices (code review, testing, monitoring), it provides comprehensive security guarantees.

---

Conclusion

Formal verification is essential but not sufficient.

What It Gives You:

• Mathematical proof protocol design is secure
• Confidence no logical flaws
• Evidence for security audits

What It Doesn't Give You:

• Implementation correctness (needs code review, testing)
• Side-channel resistance (needs timing analysis, platform hardening)
• Computational guarantees (needs crypto research monitoring)
• End-to-end linking (needs integration testing)

Best Practice: Combine formal verification with:

• Code review and testing
• Timing analysis and fuzzing
• Performance testing
• Integration testing
• Security monitoring
• User education

Result: Comprehensive security from protocol design to production deployment.

---

Further Reading

On Formal Verification Limitations:

• Dolev-Yao Model Assumptions
• Protocol Verification Scope
• Formal Methods in Practice

On Cryptographic Hardness:

• Post-Quantum Cryptography
• Cryptanalysis of ECC
• NIST Crypto Standards

On Side-Channel Resistance:

• Constant-Time Programming
• WASM Security
• Timing Attacks Explained

On Integration Testing:

• ML-KEM Security Audit
• Signal Protocol Audit
• Technical Formal Verification

---

Related Documentation

• Signal Protocol Security Audit: audit README.md
• Implementation Alignment: 06 Implementation Alignment
• Security Properties: 05 Security Properties
• All ProVerif Models: 04 All Models

---

Document Version: 1.0
Document Date: February 2026
Last Updated: February 2026
Disclaimer: This document outlines limitations as of document date. Crypto and security research is ongoing.

---

Remember

Formal verification proves the protocol design is secure. To ensure implementation security, you MUST also:

1. Test your code thoroughly
2. Review code for bugs
3. Analyze timing side-channels
4. Monitor cryptographic research
5. Test performance under load
6. Educate users on security best practices

Formal verification is a tool, not a magic wand. Use it in combination with other security practices for comprehensive security.