Today we’re releasing Verifpal 0.31.2 which represents the most significant upgrade to Verifpal’s analysis engine since its inception. The headline result: for the first time, Verifpal can fully verify a model of Signal’s X3DH key agreement and Double Ratchet protocol across three messages, under an active attacker, and it terminates in minutes.

The verified models are published on VerifHub:

• signal.vp — Guarded long-term keys
• signal_unguarded.vp — Unguarded long-term keys

This isn’t a novel research result: I myself analyzed a similar Signal model using ProVerif back in 2016 — a full decade ago. Tools like ProVerif and Tamarin have been able to handle models of this complexity for years.

But Verifpal was never built to compete with ProVerif or Tamarin. It was built as a learning tool — accessible to undergraduates and first-year graduate students who are encountering protocol verification for the first time. What matters is that Verifpal can now handle models complex enough to be pedagogically interesting, and Signal is the canonical example.

What the Models Show

The Signal model captures the full three-message flow: X3DH key agreement followed by two rounds of Double Ratchet.

Message 1 (Bob → Alice): Pre-key bundle. Bob publishes his long-term identity key, a signed semi-static pre-key, and a one-time pre-key. Alice verifies the signature and computes a master secret from four Diffie-Hellman computations — the core of X3DH.

Message 2 (Alice → Bob): Initial ciphertext. Alice derives chain and message keys via HKDF, then encrypts her first message using AEAD with associated data binding both parties’ identity keys and her current ephemeral key.

Message 3 (Bob → Alice) and Message 4 (Alice → Bob): Double Ratchet. Each subsequent message introduces a new ephemeral key, performs a DH ratchet step, and derives fresh encryption keys through the HKDF-MAC chain.

After all messages are exchanged, the model enters a post-compromise phase where both Alice’s and Bob’s long-term private keys are leaked, testing forward secrecy.

Guarded Model Results

In the guarded model, long-term identity keys are distributed over an authenticated channel (denoted by [brackets] in Verifpal syntax, meaning the active attacker cannot substitute them):

Query	Result
confidentiality? m1	Pass
authentication? Alice -> Bob: e1	Fail
confidentiality? m2	Pass
authentication? Bob -> Alice: e2	Pass
confidentiality? m3	Pass
authentication? Alice -> Bob: e3	Pass

Five of six queries pass. The single failure — authentication of Alice’s first message to Bob — is a well-known property of the X3DH handshake. Because X3DH is designed for asynchronous messaging (Bob may be offline when Alice initiates), Alice’s first message cannot be fully authenticated until Bob responds and the ratchet completes a full round-trip. This is documented in the Signal specification and is not a vulnerability; it’s an inherent tradeoff of the asynchronous design.

All three confidentiality queries pass even after long-term key compromise, confirming that the protocol provides forward secrecy.

Unguarded Model Results

In the unguarded model, long-term identity keys are sent over an unauthenticated channel, allowing the active attacker to substitute them:

Query	Result
confidentiality? m1	Fail
authentication? Alice -> Bob: e1	Fail
confidentiality? m2	Fail
authentication? Bob -> Alice: e2	Fail
confidentiality? m3	Fail
authentication? Alice -> Bob: e3	Fail

All six queries fail. When an active attacker can man-in-the-middle both parties’ long-term identity keys, every security property collapses — confidentiality and authentication alike, across all three messages. This is the expected and correct result: without an authenticated channel for identity key distribution, no amount of cryptographic ratcheting can save you.

Why Verifpal Couldn’t Do This Before

Verifpal’s active attacker analysis works by systematically mutating protocol values to candidate replacements drawn from the attacker’s knowledge. For each mutation combination, the engine checks whether the attacker can derive secrets, forge messages, or break authentication. The problem is combinatorial: as models grow in complexity, the number of mutation combinations explodes.

Two sources of explosion were responsible for non-termination on the Signal model:

Mutation Map Cartesian Product Explosion

The mutation map associates each mutable constant with a list of candidate replacement values. Previously, the verifier enumerated the full cartesian product of all mutation lists simultaneously. For a model where four constants have mutation lists of sizes [2, 7, 7, 527], the full product is 51,646 combinations — each spawning a goroutine. At higher analysis stages, where injection expands these lists further, the product grows into the hundreds of thousands.

Injection Cartesian Product Explosion

The injection engine constructs candidate primitive values by combining known values into each argument slot. For a three-argument primitive like AEAD_ENC where the attacker knows 20+ values per slot, the cartesian product can exceed 8,000 injected values — per primitive, per stage, per principal.

Together, these two explosions caused the verifier to spawn millions of goroutines on the Signal model, leading to memory exhaustion, goroutine stack overflow, or effective non-termination.

The Fixes

Weight-Ordered Mutation Scanning

The core architectural change replaces brute-force cartesian product enumeration with a weight-ordered scanning strategy that explores mutations in layers of increasing complexity.

Injection cap. A hard limit of 500 injected values per primitive (maxInjectionsPerPrimitive). The injection loop now pre-computes the total product size with overflow-safe arithmetic and breaks early once the cap is reached. This prevents memory exhaustion from a single inject() call while preserving enough injection diversity for attack discovery.

Mutation map subsetting. Two new functions — mutationMapSubset and mutationMapSubsetCapped — allow the scanner to extract and budget-constrain subsets of the full mutation map. When a subset’s product exceeds the cap, each dimension is truncated to the nth root of the limit (computed via binary search), distributing the budget evenly across dimensions.

Weight-ordered scanning. The new verifyActiveScanWeighted function replaces direct cartesian product enumeration:

• Weight 1: Each mutable variable is tested alone, capped to 50 mutations per variable. This catches attacks that require substituting only a single value.
• Weight 2: Each pair of variables is tested simultaneously. Pairs whose product exceeds 20,000 are skipped entirely (not truncated), preserving the combinatorial structure of pairs that fit.
• Weight 3: Each triple of variables, same skip logic.
• Full product: Only attempted if the total product across all variables is within 50,000.

A per-principal-per-stage scan budget of 20,000 (tracked via atomic counter) prevents any single stage from consuming unbounded work. At most 50 subsets are scanned per weight level, preventing combinatorial blowup in C(n, k) when the number of mutable variables is large.

The maximum stage limit was also reduced from 64 to 8, ensuring the verifier declares exhaustion sooner when higher stages stop discovering new knowledge — critical for multi-phase models where phase 0 must exhaust before phase 1 analysis can begin.

Lock-Free Concurrency and Hash-Based Lookups

The second fix targeted performance bottlenecks in the multithreaded analysis engine.

Lock-free attacker state snapshots. The attacker state — the central data structure tracking everything the attacker knows — was previously guarded by a read-write mutex that became a bottleneck under high concurrency. The new implementation uses atomic.Pointer[AttackerState] to publish immutable snapshots on every write. Read-side operations (attackerStateGetRead, attackerStateGetExhausted, attackerStateGetKnownCount) now try the snapshot first, avoiding the read lock entirely. Write-side operations use optimistic double-checked locking: check under read lock, then acquire write lock only if necessary.

Hash-based O(1) value lookups. The valueEquivalentValueInValues function — which checks whether a value already exists in the attacker’s known set — was a linear scan called in every hot path. It’s now replaced by valueEquivalentValueInValuesMap, backed by an FNV-like hash map (map[uint64][]int). Dedicated hashers handle primitives, equations, and constants, with special handling for the commutativity of three-element DH equations. The attacker state’s KnownMap is maintained alongside the known values list and included in atomic snapshots.

Principal state clone optimization. constructPrincipalStateClone previously deep-copied every slice in the principal state. Since several slices (Constants, Guard, Known, Wire, KnownBy, DeclaredAt, MutatableTo, Phase) are immutable after initialization, they’re now shared by reference.

Parallel stage execution. Analysis stages now run two at a time when possible, improving throughput on multi-core machines.

AEAD Check Semantics and the Final Bug

The last release fixed a subtle bug in how checked AEAD primitives were interpreted. In Verifpal, AEAD_DEC(k, c, ad)? (with the ? suffix) means the decryption is checked — the principal verifies that decryption succeeded and aborts if it doesn’t. Without the ?, the principal blindly accepts whatever comes out.

The authentication and freshness query handlers were not correctly distinguishing between checked and unchecked AEAD decryptions, causing incorrect pass/fail indices. The fix adds an early-continue path for non-checked primitives in queryAuthenticationGetPassIndices and queryFreshness.

The Signal model itself was also corrected: three AEAD_DEC calls that should have been checked (with ?) were missing the suffix, masking authentication failures that the analysis should have detected.

This was the fix that made the Signal model terminate with correct results.

What This Means for Verifpal

Once more, before academics try to strangle me (again): verifying Signal is not new. ProVerif could do this in 2016. Tamarin can do it. CryptoVerif can do it. Verifpal reaching this milestone in 2026 is not a claim of parity with these tools.

What it is, is a claim of relevance. Verifpal is used in university classrooms to teach protocol verification to students who have never seen a formal method before. When a student asks “can we model Signal?”, the answer is no longer “not in Verifpal.” That matters.

The performance improvements also benefit every other Verifpal model. Analysis that previously timed out or exhausted memory will now terminate. Models with multi-argument primitives and complex key derivation chains — the bread and butter of real-world protocols — are now within reach.

Verifpal 0.31.2 is available now. You can install it via Homebrew, Scoop, or download it directly from verifpal.com.