Verifpal 1.5: Auditing the Verifier with Frontier AI Models

Today we’re releasing Verifpal 1.5, focused on the correctness of the verifier itself. Over six commits, we used frontier AI models to audit the engine, reproduce errors in small protocol models, and develop fixes. The work found false attack reports, attacks the search missed, a crash, and explanations that said more than the underlying trace justified. It added 39 regression models.

Heba Ajjour, from University College of Applied Sciences, Gaza, Palestine, reported the halt bookkeeping bug that prompted this work. We wanted to know where else the engine might be treating a message as delivered, spending a key before it leaked, or combining values from incompatible executions. We worked with Claude Fable 5.1 and Claude Opus 5, assigning AI auditors to different regions of the engine.

Some fixes were a few lines. The hardest required changing what it means for the attacker to know a value. Along the way, the existing test harness rejected patches that fixed the example in front of us while losing real attacks elsewhere.

Where Verifpal fits alongside ProVerif and Tamarin

Our comparison of Verifpal, ProVerif, and Tamarin explains the choices behind these tools: how many sessions they cover, whether analysis always finishes, and what their answers establish. Those choices help explain both the purpose of Verifpal and the work in this release.

For sufficiently expressive symbolic protocol models, secrecy with unbounded sessions and fresh nonces is undecidable. A general algorithm cannot guarantee coverage of arbitrarily many sessions, termination on every input, and a correct yes-or-no decision every time. The comparison illustrates that constraint with this triangle:

ProVerif reasons through an abstraction. It translates processes into Horn clauses, allowing proofs over unbounded sessions. The abstraction can also admit derivations that do not correspond to an executable attack. If ProVerif cannot reconstruct a trace, a result such as cannot be proved is inconclusive. It does not establish that the protocol is insecure. ProVerif has termination guarantees for particular protocol classes, but no general guarantee for every model.

Tamarin represents state explicitly and solves constraints on executions. It can establish unbounded proofs and supports richer algebra and temporal properties. Many models run automatically; harder proofs may need lemmas, invariants, induction, or interactive guidance. Its search can also continue indefinitely. The comparison includes examples of that proof work, with links to the original studies.

Verifpal performs a finite attack search. You supply the protocol, assumptions, and queries, without helper lemmas or proof strategies. The language provides a fixed set of cryptographic primitives, and the default analysis considers two sessions per principal. The search terminates, although large models can take substantial time. It can also miss attacks within the chosen session bound, so finishing a search does not establish their absence.

That makes Verifpal useful for exploring a design: change a key’s authenticity, a peer’s identity, or the timing of a compromise, then inspect the resulting trace. A project requiring an unbounded proof needs a tool that can provide one. Verifpal can help clarify the model before that proof work, but the assumptions and properties must survive the translation. In particular, Verifpal’s equivalence? compares resolved values, and unlinkability? looks for a concrete link witness; neither establishes observational equivalence.

The full comparison covers these differences, examples of proof effort, and how to choose a tool. Version 1.5 improves the fidelity of Verifpal’s search and its explanations within that scope.

Giving the audit something to test

Verifpal takes a description of a cryptographic protocol and searches for attacks against queries about confidentiality, authentication, freshness, unlinkability, and equivalence. Its active attacker can replace messages, replay traffic across sessions, and use protocol participants to compute things it cannot compute alone.

That creates two directions in which the implementation can be wrong. It can report an attack that no execution of the model permits. It can also fail to propose a sequence of actions that would break the protocol. Fixing one direction can make the other worse.

The audit used a repeated process: inspect a region of the engine, build a minimal model that isolates a suspected mistake, explain the expected result from that model, and check the proposed change against the wider corpus. Many findings have a companion model differing in one crucial detail: a key leaks earlier, a relay is guarded, or an oracle includes a domain separator. The pair tests the boundary the fix is supposed to enforce.

The AI auditors worked across the Rust implementation and the protocol language. They could turn a suspicion about an internal check into a short .vp file exercising it. Once that file existed, we could inspect the trace and test a patch against a concrete claim.

Our existing metamorphic harness supplied another kind of evidence. It changes a protocol in ways that should have predictable effects:

• Removing a message guard gives the attacker more control, so an existing attack must remain discoverable.
• Leaking another secret must not make an attack disappear.
• Adding a concurrent session must preserve attacks available with fewer sessions.
• Renaming identifiers must leave the verdicts unchanged.

These checks can expose a missed attack without our having written down that attack in advance. They also give an audit agent immediate feedback when a proposed restriction is too broad.

Verifpal separates attack search from validation: the solver proposes message substitutions, and the engine re-executes them before recording a result. That separation is useful, but the execution and knowledge bookkeeping are themselves code that can be wrong. This audit covered those parts too.

Messages that were never sent

Consider Alice, Bob, and Carol. Alice checks a signature, then sends Bob a ciphertext. Bob unwraps it and forwards the contents to Carol.

If Alice’s check fails, she never sends the ciphertext. Bob therefore cannot unwrap and forward that ciphertext. An earlier version of the engine could nevertheless give Bob’s outgoing value to the attacker: it checked whether Bob had halted, without fully accounting for the message that Alice had never delivered.

The problem appeared in two places. When initializing attacker knowledge for a protocol phase, Verifpal could publish an outgoing value whose input never arrived. Later, its deduction engine could resolve a message name through a computation that another principal’s halt had prevented. Both could produce false disclosures.

The first audit commit introduces a shared calculation of which computations were reached, accounting for whether their inputs were delivered. It follows dependencies through relays and applies them across principals’ views of the protocol. Computing a ciphertext before a failed check does not make it public if the send comes after the check.

The companion tests exercise the opposite case. In a scenario involving a corrupt peer, the attacker may possess the key needed to replace a failing signature with one that passes. Alice then really does send, Bob really does receive, and his forwarded message becomes available. The engine now propagates those newly reached sends, updates recipients with the sending executions’ actual halts, and learns what the recipients subsequently disclose.

That distinction matters: treating everything downstream of an initially halted run as permanently unavailable would hide genuine attacks. The halted_peer_relay model and its guarded companion require both sides to work.

The audit also corrected how this bookkeeping treats declared knowledge. A principal can already know a constant through its own knows declaration, even if another principal halts before declaring the same name. The engine now credits that independent knowledge before checking whether another principal’s computation was reached. A failed computation can withhold its output; it cannot take away something another participant already knows.

Keeping deliveries and time straight

Another missed attack began with an ordinary pair of messages:

Carol -> Alice: gc
Carol -> Bob: gc

Both carry the same named value, but an active network attacker can replace only the delivery to Bob. The old search often substituted the value for every unguarded recipient at once. If Alice and Bob both computed a hash from their copy, both hashes changed together, hiding the possibility that they could disagree.

The new search includes substitutions addressed to one recipient. In split_delivery_equivalence.vp, Alice keeps Carol’s share while Bob receives a key chosen by the attacker. Their derived values now differ, as the model permits. Related tests cover forged messages and a recipient re-encrypting a secret under the substituted key.

Relays made this fix more subtle. If the actual path is:

Carol -> Alice: gc
Alice -> Bob: [gc]

then changing what Alice receives also changes what she forwards. The brackets protect the second delivery against replacement; they do not restore Carol’s original value. The second pass stopped the search from inventing independent copies along that path.

The restriction applies to the delivery whose independence matters. Bob can still receive a different value from Alice even if he later forwards his copy to Dave. A further regression model checks that forwarding alone does not exclude a recipient from this search.

Timing had a similar blind spot. One probe has Alice send a nonce to a server, the server produce a ticket for Bob, and Bob answer with a nonce of his own. The apparent attack replaced Alice’s first nonce with Bob’s later one. At one session, that requires Bob’s answer before the exchange that produces it.

The causal check had looked only at messages received by the principal currently being re-executed. Alice’s first message went to the server, so a search running against Bob found no matching receive and skipped the restriction. It now checks availability before the earliest delivery to every principal the substitution reaches.

The resulting tests make the timing concrete. causal_foreign_receive.vp holds at one session. Leak Bob’s nonce before the exchange and an attack is found. Add a second session and a nonce from that other run can also make an attack possible. A rule that simply rejected this shape would get those cases wrong.

The same care applies when a value has several derivations. A tag observed from an oracle and a tag constructed using a leaked key may be equal, but the leak can occur too late for the attack being considered. The audit aligned the checks on causality and execution history so that switching to an alternate derivation does not bypass those restrictions. Alternate observations are considered only when the primary route leaves the value unavailable, and they must satisfy the relevant visibility, dependency, and history checks. Trying every alternate on every call tripled analysis time during development.

Teaching the search to start an attack

Some attacks were absent because the solver tried to do too much at once.

In solver_oracle_input_prefix.vp, Bob computes a message authentication code (MAC) over an input and sends the tag back. Later, he accepts a message accompanied by a MAC over a particular structure. The attacker can exploit Bob’s first operation as a MAC oracle: send it the structure the later check expects, collect the tag, then use it.

The solver proposed the oracle input and the final forged message together. Validation correctly refused: the attacker did not yet possess the tag. But the search never proposed just the first step, so the attack stopped before it began.

The fix lets a refused proposal yield the portion whose substitutions are already controllable, derivable, and available in time. Re-executing that portion produces the oracle output; a later search round can finish the attack. This fallback is limited to the oracle chains it is meant to help. An unrestricted version made the userbase.vp model ten times slower.

The solver also learns which inputs to ask for by matching what a principal can emit against what checks elsewhere in the protocol require. That finds cases where the useful shape comes from a third participant, where a chosen salt changes a derived key, or where a certificate authority signs an attacker key supplied in a field intended for a name.

The next pass extended this to nested shapes. One new model asks Bob to verify:

MAC(k, MAC(k, CONCAT(nb, nc)))

Alice and Dave each hold k and will MAC the input they receive. The attacker can build Bob’s expected tag in stages:

1. Give Alice CONCAT(nb, nil) and collect the inner MAC.
2. Give Dave that MAC and collect the outer MAC.
3. Deliver nil as nc, accompanied by the resulting tag.

Here nil is a public symbolic value the attacker can use. The search now considers the inner expression as well as the final one, so it can discover the first request. The companion model gives the two oracles distinct domain separators: fixed labels included in their MAC inputs. Their outputs no longer have the required shapes, and the authentication query holds at both tested session counts.

Two other changes recover attacks that existing machinery was accidentally excusing. The authentication checker recognizes when a received message could have come from a legitimate sender run. Its test for independent attacker forgery used to remove every value read from the sender’s assignments, including a leaked derived key or an ordinary public key. That could make a message the attacker built look as though it required the sender. It now distinguishes computations dependent on received inputs from those based on the sender’s own static and fresh data.

The deduction engine also used to reject a combination when its first recorded derivations conflicted, even if an alternate observed derivation made the combination possible. Imagine asking Bob for one tag and Dave for another: recording both tags first through Bob must not force the eventual attack to obtain both from the same Bob run. The engine and trace minimizer now consider compatible alternate routes. This also uncovered a real disclosure with two sessions in the existing closure_cyclic_union.vp regression.

Values need to remember which execution produced them

The largest change concerns a false attack that survived several narrower approaches.

In the regression model, Bob publishes a key for a key encapsulation mechanism, or KEM. Alice encapsulates to it and sends Bob the ciphertext. Bob decapsulates and encrypts a private reply under the resulting shared secret.

There are two relevant executions:

The old engine could combine knowledge from those incompatible executions and report that the reply had been disclosed. Earlier history checks caught direct conflicts, such as two reads requiring different values in the same received slot. Here the conflict was deeper in the derivation: the stored knowledge did not fully describe which executions could produce each ingredient.

Seven attempts to repair this by tightening an existing check traded the false report for a missed attack. A recurring problem was that rejecting a recorded derivation also discarded a value the attacker could obtain another way. Requiring every replayed read to return exactly its recorded value, for example, lost an attack in the Needham–Schroeder model when a guard was removed.

The final commit changes the representation of knowledge. Each learned value carries a set of possible worlds: constraints describing the executions that produce it. A constraint can say that a particular principal received a particular value in a particular message slot. A value may have several compatible ways of being obtained.

When the engine combines ingredients, it merges those constraints. If every combination requires contradictory values at the same principal and slot, the derivation is refused. In the KEM example, the constraints for the reply and the alleged opening secret cannot be combined.

Two details prevent this from becoming another overly broad rejection rule. First, a value constructible from knowledge available in every execution gets an unconstrained world. Its availability must not depend on whichever derivation happened to be recorded first. Second, finding a value already known inside a private computation does not establish a new observation. The engine widens the possible worlds through such a read only when the corresponding slot travels over the wire or leaks.

The tests include a Diffie–Hellman exchange where replacing a share really does reveal one encrypted message, while a later message remains protected. The revised engine reports the first disclosure and rejects the second. That pair helps check that the repair preserves a real attack through key substitution.

There is a deliberate cost limit. An unbounded implementation made the threshold ring stress model 32 times slower. The committed version retains at most sixteen worlds per value, bounds the merge search, and caches results as knowledge changes. The commit records 19.6 seconds against a baseline of 15.9 seconds on that model, with overhead below 5% on the ordinary models measured.

At either limit, this additional filter drops the constraints and allows the candidate through to the remaining checks. It can therefore miss an inconsistency; reaching the limit cannot itself reject a real derivation. Those bounds are part of the implementation’s limitations, and the fix should not be read as an exhaustive solution to execution compatibility.

Smaller mistakes with significant consequences

Re-sharing a secret was treated as repeating the same sharing. Consider two separate assignments:

s1, s2, s3 = THRESHOLD_SPLIT[2](k)
t1, t2, t3 = THRESHOLD_SPLIT[2](k)

Learning s1 and t2 does not meet either threshold: the assignments represent independent sharings. The engine previously treated them as one family and could reconstruct k. A field in the primitive specification now marks operations whose assignments need distinct identities, and those identities participate in term comparison and hashing. The regression model keeps k confidential at one and two sessions.

Bypassing one check could accidentally rewrite another principal’s signature. After recognizing that an attacker knew an encryption key, a bypass round resolved a state that had already been resolved. That could reinterpret Alice’s SIGN(sk, x) through Bob’s substituted copy of x, effectively changing what Alice had signed. Each round now starts from the state before resolution, applies all bypasses accumulated so far, and resolves once. The test preserves the distinction between breaking encryption with a leaked key and forging a signature under an uncompromised one.

Public identifiers could make an honest peer appear corrupt. Scenario handling treated generated values as secrets, so publishing an identifier or salt could mark a peer as compromised and exclude its run’s queries. Corruption inference now considers the value’s role as key material, using the primitive registry. A generated identifier sent in cleartext no longer removes the very query that would expose an attack.

A relationship imposed by the attacker could count as a privacy failure. Forcing two encryptions to use a key of the attacker’s choosing does not demonstrate that the attacker recognized a secret relationship between their honest versions. Unlinkability witnesses, apart from observed equality, now have to carry a secret leaf from a subterm the honest queried values actually share. This removes the false link in unlink_forced_key_carries_no_secret.vp.

A solver resource limit could abort the analysis. Two concurrent BAN–Yahalom runs exhausted one solver lane’s supply of fresh variables. The lane now stops generating further proposals instead of aborting the process or allocating identifiers from another lane’s range. This is a search bound, so avoiding the crash does not imply that the exhausted branch was fully explored.

Checking the conditions and the explanation

Queries can restrict themselves to executions in which a named message is sent. For example, a confidentiality query may apply only after Bob sends an acknowledgement.

One bug resolved that message name against the state answering the query. If that state had been truncated at a failed check, a later declaration from an unrelated participant was missing, and the engine dropped the verdict. The name now resolves against the protocol trace, where it belongs.

Another bug asked the wrong execution whether the send happened. An attacker can replace Bob’s public share, learn a secret that Alice encrypts, and also cause Bob’s decryption to fail. Alice’s state may reveal the confidentiality violation without containing Bob’s later halt. Consulting only Alice’s view allowed a query gated on Bob’s acknowledgement to fail even though Bob never acknowledged anything.

The precondition fix replays the substitutions recorded with the disclosure and checks the sender’s state in that execution as well. In the regression, the unrestricted confidentiality query still reports the disclosure; the query requiring Bob’s acknowledgement does not. This additional replay applies to confidentiality, while the other query kinds retain their existing execution check.

Finally, a correct verdict can still have a misleading explanation. While modeling SPLICE/AS, the audit found a trace claiming that a guarded message had been altered on an earlier unguarded hop. In that case, the sender created the value: the supposed earlier hop did not exist.

The narration change checks for an actual earlier unguarded delivery to that sender before making the claim. It removes the unsupported justification; it does not change the verdict about the certificate swap or erase the reported substitution. The explanation remains for relay models where the earlier hop really exists.

What ships in 1.5

The final commit reports a passing suite of 1,385 tests, along with successful exhaustive metamorphic sweeps, lint and formatting checks, and a working WebAssembly build. The audit also compared result codes at one and two sessions and inspected differences in the full output, including changes to attack witnesses. Existing corpus verdicts were largely stable; the disclosure with two sessions in closure_cyclic_union.vp was an explicit change, alongside the new regression cases.

Several plausible fixes failed those checks. One proposed restriction on FROST partial signatures removed a false forgery but lost three existing attacks when a guard was removed. Another stricter history rule lost both a receipt forgery and a replay against a key confirmation exchange. Both were reverted. Keeping those failures in the commit messages records what a future repair still has to preserve.

These six commits also leave findings open. The audit recorded a missed attack on Woo–Lam Pi using parallel sessions, a replay classified as a duplicate acceptance without establishing whether the other recipient had accepted, and a remaining precondition case involving a sender deprived of an input without itself halting. They should not be counted as fixed by this work.

Verifpal remains a bounded and incomplete search: two sessions per principal by default, and a passing query means no attack was found under the search performed. The audit strengthens the implementation and gives us more precise regression cases; it does not turn a pass into a proof of protocol security.

The AI auditors helped turn suspected code paths into small protocols we could run and inspect. Those protocols are now part of the repository: future changes must still distinguish an early leak from a late one, preserve the real oracle attack, and reject the disclosure assembled from incompatible executions. Verifpal 1.5 includes both the fixes and these regression models. You can get it from the Verifpal releases page.