Verifpal Reaches 1.0: A Toy Becomes an Instrument

Verifpal 1.0 is out. Since May 2020, Verifpal has printed the same warning at the top of its analyses: Verifpal is Beta software. Version 1.0 deletes that line. What justifies the deletion is a new paper, Verifpal Seven Years Later: Can a Toy Become an Instrument?, the successor to the 2019 paper that introduced the tool. Two things have changed since then, and the paper accounts for both: what the modeling language can express, rebuilt across last week’s 0.70.0 and 0.80.0 releases, and whether the engine’s answers deserve belief. This post is the whole argument in one place.

The 2019 paper was frank about what it was presenting. It described its own soundness argument as “an incomplete, semi-formal, in-progress set of results,” called its unlinkability queries “especially experimental,” and conceded that its completeness argument rested on “the problematically subjective definition of what constitutes a ‘real-world protocol’.” The reasonable conclusion at the time was that ProVerif and Tamarin were verification tools, and that Verifpal was a teaching aid that resembled one. The blunter version, which the new paper’s title takes up rather than disputes, was that Verifpal was a toy.

Seven years later, the paper re-asks the question, and it tries to answer it the way a skeptic would want it answered: by proving what can be proved, measuring what can be measured, and conceding in print what can be neither.

What the language can now say

A tool that cannot express the protocol in front of you is of no use whatever its theory, so the paper’s first answer to its own question is a list of what the language now covers. The items landed across 0.70.0 and 0.80.0, each of which has its own detailed post; here is the short version.

Diffie-Hellman stopped being special

The 2019 language had a third kind of value alongside constants and primitives: equations, written G^a and G^a^b, with a reserved generator, a limit of two exponents, and their own special case in the parser, the printer, the equational theory, the unifier and the search. They modeled Diffie-Hellman and nothing else. That kind of value no longer exists. Key exchange is written with two ordinary primitives, PUBKEY(a) and DH_KEX(ga, b), and commutativity is a declared field on the primitive’s specification, interpreted by the same machinery as every other rule. The equivalence relation is arranged so that DH_KEX(PUBKEY(a), PUBKEY(b)), the term an attacker can build from two public keys off the wire, is equivalent to no shared secret: the computational Diffie-Hellman assumption, made structural in the term algebra instead of handled as a special case in the engine.

Post-quantum and hybrid key exchange

Removing equations was the precondition for this. A KEM has no exponent to commute, so it could not be expressed through the equation interface at all. KEM_ENCAP and KEM_DECAP are thirty-eight lines of declarative data, absorbed by the rest of the engine without modification, and they make the question we hear most often since recommending post-quantum native design something a model can settle: what does a hybrid actually buy you? Three shipped models are the same protocol, an X25519 leg and a KEM leg fed into one key schedule, differing only in what phase 1 leaks:

It is the hybrid construction argument as three files you can run in a design review.

Assumptions you can declare, verdicts that carry them

From 0.80.0, a call site can state a weakening assumption directly instead of approximating it with a hand-maintained list of leaked values: SIGN[forgeable](sk, m) costs authenticity, AEAD_ENC[weak](k, m, ad) costs confidentiality, and from phase 2 schedules the break, which is exactly what a harvest-now-decrypt-later adversary is. Scheduling comes with an obligation the paper formalizes: knowledge acquired in a later phase must never justify an action taken in an earlier one, or any key ever leaked would forge any signature ever checked. The annotations feed the ordinary deduction rules, and the design shows in what we did not have to write: once PUBKEY[weak] hands the attacker a private value, the existing reconstruction machinery recomputes every shared secret that value was ever used in, with no Diffie-Hellman-specific rule anywhere.

Two decisions govern how the feature behaves at its edges. An annotation a primitive does not declare is a hard error at load time with an explanation, because an annotation that reads like a check but does nothing is more dangerous than no annotation; malleable parses and is rejected on those grounds, held back until the solver can actually find the two-substitution attacks it would advertise. And every verdict obtained under assumptions is printed beneath the assumptions in force, which travel through the JSON interface too, so a Pass under PUBKEY[weak from phase 1] cannot be quoted as a Pass outright:

  Warning ▲ Analysis performed under 5 declared weakening assumptions:
  Warning ▲ PUBKEY[weak from phase 1](alongterm)
  Warning ▲ PUBKEY[weak from phase 1](blongterm)
  Warning ▲ PUBKEY[weak from phase 1](bs)
  Warning ▲ PUBKEY[weak from phase 1](bo)
  Warning ▲ PUBKEY[weak from phase 1](ae1)
 
     Pass ✓ confidentiality? m1
     Pass ✓ authentication? Alice -> Bob: e1

The model behind that output is PQXDH, Signal’s current session setup, with every Diffie-Hellman public key annotated weak from phase 1 and nothing leaking at all. The one line to look at is the KEM encapsulation key, which carries no annotation. That omission is the hybrid argument in its entirety: discrete logarithm falls, the KEM does not, and the message survives on exactly that difference.

Unlinkability, decided by finding a witness

unlinkability? used to be decided by structural tests that never consulted what the attacker had observed. It is now decided the way the manual always defined it: by searching for a concrete link witness, a value in the attacker’s hands that ties both queried values to one participant, which the trace then reports as the explanation. In the DP-3T contact-tracing model, a leaked day-zero seed links every identifier that phone will ever broadcast, and the trace names the seed, so the fix is visible in the result. The specification table records which argument positions identify a participant, which is how the engine knows that two signatures verifying under one key are linkable while two ring signatures over the same ring are not: a successful ring verification names a set of possible signers and never a member of it, and that declared emptiness is what stands between this query and a false attack on the one primitive whose entire purpose is unlinkability.

Soundness, assuming the solver is broken

The active-attacker search is the part of a symbolic verifier where the difficulty lives, and therefore the part where the bugs live. The 2019 engine searched forwards, enumerating combinations of wire values to tamper with under four tuned parameters, and those parameters, rather than the protocol under analysis, decided which attacks were reachable. The 0.70.0 post describes its replacement: a backward search that starts from each unresolved query and works out what the attacker would need to contradict it.

The paper’s job is different: to say why anyone should believe what that search reports. Its answer is not a correctness proof for the solver. “The theorem we want,” it says, “is not that the solver is correct, but something stronger and easier to check: that the solver’s correctness is irrelevant to soundness.”

The theorem treats the solver as an arbitrary function, an adversarially buggy one included, and shows that a reported attack is real anyway. The structure that makes this provable is the one 0.70.0 shipped: the solver can only propose. Before anything reaches you, a much smaller component checks that the attacker controls every wire slot the proposal writes to, re-derives every term it installs from the attacker’s own knowledge, re-executes the protocol with the substitution in place, and re-tests the query against what the attacker then holds. Recording a query result requires a token whose constructor is private to one module, so “the search cannot record anything” is a fact the Rust compiler enforces rather than a discipline we promise to maintain.

The paper then does the accounting that a claim like this owes its reader.

Writing the deduction rules down as an inference system, which the paper required, also found a bug. The closure’s decomposition rule demands that the attacker actually hold a term before opening it, and holding k makes ENC(k, m) openable without making it obtainable: producing it still requires m. A helper in the engine had conflated the two, and on a forty-line model the tool reported the attacker decrypting under a key that the same run separately certified it could not obtain. A false attack, in the passive analysis, with no solver anywhere near it. The repair is one premise in one rule, decompose_is_not_construct.vp now pins it in the test suite, and the episode is in the paper because it is the best evidence we have for doing this kind of writing-down at all: the formalization caught what the test suite had not.

The model that would not finish

A verifier that does not terminate is worse than useless, because you cannot tell a hard protocol from a broken tool. Symmetric-key Needham-Schroeder ships in Verifpal’s examples directory, and for five years, across two implementations of the tool, it did not finish: the analysis ran for minutes without resolving a single query.

The cause turns out to be a clean pattern the paper calls a replay pump. The protocol decrypts a value, hashes it, and encrypts the result under the same key, so its own output is a well-typed input to itself, one level deeper. An attacker that replays the output into the input obtains a term it did not previously hold; the analysis counts new knowledge as progress and goes around again; the next round produces a term nested one level deeper still. On Needham-Schroeder the engine climbed to 213 nested hash applications and roughly 132,000 proposals in its first 45 seconds, with no end in prospect.

What stops the pump in 1.0 is a bound that is read off the model rather than chosen: the attacker may not install a term that nests deeper than anything the protocol itself computes. A protocol that builds deeper values gets a deeper bound (across the shipped corpus it ranges from 4 to 20), and there is nothing to tune. Symmetric-key Needham-Schroeder now completes in about a tenth of a second at one session and 2.4 seconds at the default two, reporting the textbook Denning-Sacco replay, and the paper proves that the analysis as a whole terminates, unconditionally.

The bound excludes a class of attacks: any whose injected term must nest deeper than the protocol builds. So the tool says so, at the exact place the exclusion occurred, without being asked:

     Info ● Search declined AEAD_ENC(k, HASH(HASH(HASH(HASH(m)))), nil) at
            Bob's e1: it nests deeper than the 4 levels this protocol itself
            computes. Attacks needing a term deeper than the protocol builds
            are out of reach.

A Pass gives you no way of knowing which branches a search declined to walk down, which is what makes undisclosed incompleteness corrosive. This disclosure names the principal, the slot, the term, and the depth the protocol itself reaches, so a reader who worries about deep-construction attacks against this protocol knows exactly where to direct the worry.

Two sessions of every principal

Protocols are deployed concurrently, and some attacks need two instances of one role to exist at the same time. The standard specimen is Millen’s fⁿgⁿ protocol, engineered so that its secrecy break requires two parallel sessions of the responder; an analysis holding one session of each principal cannot even state the attack. This class of protocol was the sharpest objection to Verifpal’s standing as a verifier, and until 0.80.1, released alongside this post, the objection was correct.

As of 0.80.1, every principal enters the analysis as two concurrent sessions of itself, so a two-party model runs as four principal states: Alice and Alice#2, Bob and Bob#2. Each session draws its own fresh values while long-term material stays shared, and the attacker is free to route any session’s traffic into any other. No model needs editing and no syntax was added, because the language has carried the necessary distinction since 2019 without using it: generates was always “fresh in each run,” and knows was always “long-term.” Raising the count is a matter of --sessions, up to 16 sessions per principal.

Here is what that buys on FFGG, Millen’s protocol at n = 2 and the very model the 2019 paper used for its own trace comparison:

     Fail ✗ confidentiality? m
            ╭─ Attack trace:
            │ 1. In an earlier session in which the attacker replaced n2#2
            │    with n1, msg2#2 resolved to PKE_ENC(pkb, CONCAT(n1, m, n1#2)).
            │ 2. Attacker replaces msg (sent by Alice to Bob) with
            │    PKE_ENC(pkb, CONCAT(n1, m, n1#2)). (msg was
            │    PKE_ENC(pkb, CONCAT(n1, n2, m)))
            │ 3. Bob's SPLIT(PKE_DEC(skb, msg))? passes — its inputs are
            │    attacker-controlled.
            │ 4. Bob's ASSERT(SPLIT(PKE_DEC(skb, msg))?, n1)? passes — its
            │    inputs are attacker-controlled.
            │ 5. Attacker observes m on the wire.
            ╰▸ m (m) is obtained by Attacker.

The two nonces in that trace are different objects: n1 belongs to one responder session and n1#2 to the other. The attacker uses the second session as an oracle, feeding it the first session’s nonce so that its reply comes back with the tuple rotated, then presents that reply to the first session, whose own checks pass and whose response moves the secret into a position sent in the clear. This is the shape Tamarin’s counterexample for the same protocol takes, and Verifpal finds and narrates it in the names the model declares.

Bounded sessions are still not unbounded replication, and the paper is specific about the two gaps that remain. First, a passing query at k sessions means that no attack was found within k sessions, never that none exists. Second, the repeated runs of any one session share that session’s fresh values, which grants the attacker an equality that true replication would withhold. The engine cannot close the second gap, so it discloses each instance of it: after minimizing a witness, Verifpal re-runs the attack with the target’s own fresh values renamed to the copies a different session would have held. A witness that survives the renaming did not depend on shared freshness. A witness that dies is still reported, with a label. Run the same FFGG model at --sessions 1 and the only route to the secret is exactly such a witness:

     Fail ✗ confidentiality? m
            ╭─ Attack trace:
            │ 1. In an earlier session in which the attacker replaced n2
            │    with n1, msg2 resolved to PKE_ENC(pkb, CONCAT(n1, m, n1)).
            │ 2. Attacker replaces msg (sent by Alice to Bob) with
            │    PKE_ENC(pkb, CONCAT(n1, m, n1)). (msg was
            │    PKE_ENC(pkb, CONCAT(n1, n2, m)))
            │ 3. Bob's SPLIT(PKE_DEC(skb, msg))? passes — its inputs are
            │    attacker-controlled.
            │ 4. Bob's ASSERT(SPLIT(PKE_DEC(skb, msg))?, n1)? passes — its
            │    inputs are attacker-controlled.
            │ 5. Attacker observes m on the wire.
            │ Note: this trace reproduces only because sessions of Bob share
            │ n1. Under per-session freshness this witness does not reproduce;
            │ an attack may still exist by another route.
            ╰▸ m (m) is obtained by Attacker.

Across the corpus, that label survives on 13 of the 153 narrated traces that involve a substitution, Scuttlebutt and TLS 1.3 among them. It asks the reader the one question the engine cannot answer for itself: can the attacker obtain this principal’s fresh value inside the very session it is attacking? For Needham-Schroeder public key the answer is yes, which is why Lowe’s attack is real even though its Verifpal witness carries the label. The label is a request for review, not a verdict.

Concurrency has a price: two sessions cost roughly four times one, because the model handed to the analysis is twice the size. Most models still finish in fractions of a second; a TLS 1.3 handshake takes 7.9 seconds; the slowest analysis in the corpus is the twelve-message Signal model at 307 seconds, which --sessions 1 brings down to 42.

Measuring whose names are in the trace

When a query falls, the thing you are shown was built in two stages. The state that falsifies one query usually carries substitutions that other queries needed, so the witness is first minimized: substitutions are dropped one at a time for as long as the violation keeps reproducing, with every probe run against a scratch context that is not permitted to record results. What survives is narrated as numbered steps of exactly three kinds: a substitution, with the displaced honest values shown in parentheses; a gate, a checked primitive that passed on attacker-controlled input, which is the step a skeptical reader most wants to interrogate and so gets a line of its own; and a derivation, read off the record the deduction rules kept as they ran rather than reconstructed afterwards by a pretty-printer guessing at what must have happened.

The other half of readability is vocabulary. The narrator keeps a table mapping terms back to the names your model gave them, which is why one step of a Signal trace reads Attacker opens e1 with akenc1, obtaining m1. while the engine’s internal record of the same fact runs to seven lines of nested HKDF, MAC, HASH and DH_KEX applications.

How readable is the result, next to what the peers produce? The 2019 paper printed Verifpal’s FFGG attack trace beside ProVerif’s and argued that the former was easier to read. The argument was impressionistic, and the trace it was defending was a state dump. The new paper re-runs that comparison seven years later, against ProVerif 2.05 and Tamarin 1.12.0, and replaces the impression with a measurement: of the identifiers in the region where each tool expresses its counterexample, once each tool’s fixed boilerplate is discarded, what fraction occur in the model the user wrote? The strict reading requires a verbatim match; the lenient reading forgives each tool its decorations, so that Verifpal’s n1#2 and ProVerif’s ~M_14 are treated alike.

Read the caveats before the numbers, because the paper insists on them. The table is not a scoreboard: under a coarser reading that counts every token, including all of Verifpal’s English, Verifpal falls to between 41.9% and 62.9% and Tamarin’s graph beats it on all three protocols, so no absolute percentage is stable, and what survives every reading is only where each tool’s renaming falls. Tamarin is measured on the trace graph it can serialize rather than on its default output, because its default output under --prove is a proof script, an artifact that is not a counterexample at all; which artifact a tool hands you by default is itself a finding. And the sharpest caveat cuts against Verifpal: the reason it can keep your names is the same reason its session count is bounded. Analyzing finitely many sessions lets it privilege the first as the one you wrote and suffix the rest, while a tool that quantifies over unboundedly many sessions has no first session to privilege and must rename every instance. Verifpal’s readability score and its central limitation have the same cause, and the paper says so in as many words.

The comparison would be worthless if the tools disagreed about the verdicts underneath, so the paper first checks agreement across fourteen properties. Twelve are unanimous among the tools that ran, and the two exceptions are examined rather than smoothed over: one is ProVerif returning cannot be proved where the other two exhibit a falsification, the stated price of the coarse abstraction that gives ProVerif its generality, and the other is a Needham-Schroeder-Lowe query on which Verifpal’s use-based authentication predicate and ProVerif’s injective agreement ask different questions and get different answers, with neither tool wrong about its own question.

One more property rides along with the measurement. Every trace Verifpal shows you was re-executed, from a pristine state, to the reported violation before being rendered, and that is a theorem in the paper rather than a habit of the implementation. In the 9 cases out of 153 where no minimized witness could be confirmed to re-execute, the trace says that too, on the trace itself.

This line of work has a specific origin: the paper’s acknowledgments credit the applied cryptography students at the American University of Beirut, “who are the readers this tool is actually for,” and whose difficulty reading attack traces from every tool, ours included, is what turned trace readability from a feature request into a research question.

What it still cannot do

The paper gives its limitations a full section, and none of them is small.

There is no observational equivalence. If the property you care about is that an adversary cannot tell two worlds apart, which is the standard formulation of vote privacy, anonymity and strong secrecy, Verifpal cannot answer it, and no combination of its queries adds up to an answer.

There are no user-defined equational theories. A protocol whose security depends on algebraic structure the built-in table does not model (XOR-based constructions, pairings, small-subgroup and invalid-curve behavior) cannot be modeled faithfully at all, and may be modeled unfaithfully without any complaint from the tool. The fixed table is deliberate, and it is the one design principle unchanged since 2019: a user-supplied theory can fail to terminate or quietly grant the attacker an equality the actual primitive does not have, no tool can tell a deliberate abstraction from a broken one, and both peers constrain their theories too, so the question was never whether the theory is constrained but who constrains it. We stand by that defense, and it does not shrink the gap. No new table row gives Verifpal XOR.

And sessions are bounded. The paper calls this the best case against everything else in it: without unbounded replication, a passing query can be weaker than it looks. We accept the case. It bears on what a passing query means, not on the attacks the tool reports, which are sound however the solver behaves, reproduce as printed, and are the attacks its peers report.

Why “instrument”

The paper chose its final word for three properties a measuring instrument has, and it checks Verifpal against each. An instrument’s readings are characterized, so that you know in which direction to trust them: Verifpal’s are characterized in one direction, since a reported attack is real whatever the solver does, and silence never means security. An instrument’s operating range is documented: the section above is the range, and the paper states it at greater length. And an instrument indicates when it is being read outside its range, which is what the labels in this post are: a declined proposal named at its slot, a shared-freshness note printed on the trace it qualifies, a verdict obtained under a declared weakening assumption printed beneath the assumptions in force.

The paper also names the one place the analogy fails, rather than leaving the reader to find it. The backward search draws whole terms only from a finite basis of terms the protocol computes, and a goal that fails for want of a term outside that basis looks exactly like a goal with no solution, so this incompleteness has no particular place to point to. An instrument’s casing states its range completely; Verifpal’s cannot. What it does instead is print the fact itself at the top of every active analysis: “Where the search needs a whole term at once, it draws only from terms this protocol computes; an attack needing one outside that set is out of reach. Unlike the other limits, this one cannot report where it applied.”

None of this makes Verifpal a substitute for ProVerif or Tamarin, and the paper does not argue that it should be one. The three tools distribute trust differently. Tamarin returns a proof object, the strongest artifact any of them produces, and a reader who can read one should prefer it; reading one, and often completing one, is expert work. ProVerif buys automation and unbounded sessions with an abstraction deliberately coarser than the concrete semantics, and tells you when that abstraction cannot decide your query. Verifpal moves the solver out of the trusted region and hands you an attack you can re-execute by hand without trusting the tool that found it. Its positive claims are the most bounded of the three; its negative claims come with the most checkable object. “A tool can be worth using without being worth using alone,” as the paper puts it; “nobody proposes retiring ProVerif on the grounds that Tamarin proves more.”

Getting it, and what 1.0 commits to

brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal

On Windows, scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git followed by scoop install verifpal. The Workbench runs the release in the browser with nothing to install, and the paper is on the IACR ePrint Archive; its artifact re-runs all three tools on every model and regenerates every number quoted above, the provenance table included.

Verifpal 1.0 adds no features over 0.80.1. It removes a sentence: the beta warning, in place since May 2020, whose job was to say that the tool’s claims about itself had not been written down. They now are, in one paper: the semantics, the deduction rules, the search, the soundness theorem and its 2,751-line residue, the termination bound, the session model, and the limits. The abstract answers the title’s question in one line: Verifpal “has become a different instrument, not a smaller one,” and it “belongs alongside its two peers instead of in their place.”

If you model something and a result looks wrong to you, please open an issue. The paper’s acknowledgments thank the Verifpal users who reported results that looked wrong, because the unlinkability rework began exactly that way. What 1.0 changes is that there is now much more for a report like that to be checked against.