Comparison

The tradeoff triangle

For sufficiently expressive symbolic protocol models, secrecy with unbounded sessions and fresh nonces is undecidable. A general algorithm cannot promise all three: coverage of arbitrarily many sessions, termination on every input, and an exact yes/no answer every time. This is a limit of the problem itself. Durgin et al. establish the undecidability result and several decidable restrictions.

The familiar “pick two” picture needs that qualification. ProVerif does not always terminate. Verifpal gives up unbounded proofs, but also uses a heuristic search within its bound: it can miss attacks at the selected session count. Bounded-session decidability results do not make Verifpal a complete decision procedure. Its research paper documents the proposal families and depth restrictions that shape the search.

Three approaches to the same difficulty

ProVerif: prove through abstraction

ProVerif translates processes into Horn clauses, an abstraction that makes unbounded reasoning tractable in many cases. Ordinary Horn facts are reusable: recording that a message can occur does not count how often it was emitted, and the clauses retain only part of each participant’s state. A clause can be applied repeatedly even where a concrete session executes that step only once. A derivation can therefore combine steps that no actual execution can perform together. Blanchet’s account of the abstraction explains how ignoring repetitions enables unbounded analysis while admitting false attack derivations.

Resolution derives the consequences of those clauses. If the secret is not derivable even in this more permissive model, it is secret in the protocol. If it is derivable, ProVerif attempts to reconstruct an execution. An unsuccessful reconstruction can produce cannot be proved, which means inconclusive, not insecure. Its output guide distinguishes proofs, reconstructed attacks and inconclusive results.

This is a powerful way to obtain automated unbounded proofs. There is no general termination guarantee, although one holds for the tagged-protocol class studied by Blanchet and Podelski. On harder models, lemmas, induction and other refinements can improve precision and help the analysis finish. Those features expand what ProVerif can establish, while sometimes adding work for the analyst.

A concrete example: symmetric-key Needham–Schroeder. The Verifpal paper’s comparison artifact records the following ProVerif 2.05 output for Bob-to-Alice authentication. The reconstruction fails at an input where its derivation attempts to reconcile different ciphertexts in the same session:

Try adding a [precise] option on it.
Trying with the initial derivation tree instead.
Could not find a trace corresponding to this derivation.
RESULT inj-event(AliceAcceptsFromBob(x)) ==> inj-event(BobSendsToAlice(x)) cannot be proved.
RESULT (even event(AliceAcceptsFromBob(x)) ==> event(BobSendsToAlice(x)) cannot be proved.)

The request for [precise] is the tool asking the analyst to help recover information lost in the abstraction. The same artifact records attack findings for the corresponding direction of authentication in Tamarin and Verifpal:

These are results from the recorded encodings, whose acceptance conditions differ. Tamarin checks a non-injective event correspondence after matching a ciphertext; Verifpal’s recorded witness reaches an unchecked decryption. The findings are not identical attacks against identical predicates. The raw evidence is in bench/outputs/needham-schroeder.{proverif,tamarin,verifpal}.txt in the paper’s artifact.

The practical distinction is visible even on this small example: an inconclusive derivation leaves the analyst with more modeling work, while a concrete finding gives them behavior to inspect against the intended protocol.

Tamarin: prove by solving constraints

Tamarin models protocol state with multiset rewriting rules and searches for executions satisfying or violating a property. Its trace analysis can establish unbounded proofs or construct counterexamples under its supported theories. Search may continue indefinitely: an obligation can generate another obligation of the same shape at an earlier point in an execution. The Tamarin manual explains both its automatic and interactive modes.

The analyst can supply induction, lemmas about where messages originate, reusable invariants, and heuristics that guide the search. Tamarin’s property language and proof controls provide considerable flexibility. Many models run automatically; difficult ones can require substantial expertise. Its explicit state and built-in algebra for Diffie–Hellman, XOR and pairings make it especially valuable when those details matter.

Even a three-message protocol can need a lemma. The comparison artifact’s untyped Needham–Schroeder–Lowe model uses a hand-written types [sources, reuse] lemma to close message-origin cases left unresolved by --auto-sources in that encoding. It follows Tamarin’s own untagged NSLPK3 example. Here is the complete lemma from the artifact’s models/tamarin/nsl-pk.spthy:

lemma types [sources, reuse]:
    "(All na m1 #i. IN_B_1_na(na, m1) @ #i ==>
        ((Ex #j. KU(na) @ #j & #j < #i) |
         (Ex #j. OUT_A_1(m1) @ #j & #j < #i)))
     &
     (All nb m2 #i. IN_A_2_nb(nb, m2) @ #i ==>
        ((Ex #j. KU(nb) @ #j & #j < #i) |
         (Ex #j. OUT_B_1(m2) @ #j & #j < #i)))"

The first half says that a nonce Bob receives either was already known to the attacker or came in an earlier first message from Alice. The second states the analogous origin condition for Alice’s received nonce. The sources annotation makes the lemma available to refine the origin analysis; reuse makes the proved result available to subsequent lemmas. The analyst has supplied a fact about the protocol that lets the remaining proof search proceed.

Automatic source generation reduces this burden on many examples. It does not guarantee a finished proof: Cortier et al.’s evaluation lists untagged NSLPK3 as needing an additional reuse annotation, and the manual requires checking both the generated lemma and whether it resolves the outstanding cases. This is part of the expertise an unbounded proof can require even for a compact protocol.

Verifpal: search within explicit limits

Verifpal combines a fixed primitive vocabulary, a finite session expansion and bounded term construction with backward search from the security question. Active-search proposals pass through a separate validator that checks attacker constructibility and re-executes the affected state before accepting a contradiction. The analyst supplies the protocol and queries, without helper lemmas or proof strategies. The paper specifies the search, validation and termination argument.

This makes a finite analysis available without first solving a proof-search problem. Termination does not promise a short runtime, and exhausting the implemented search does not prove security. Verifpal’s useful product is an inspectable finding, together with an explicit account of the search and assumptions behind the result.

The case for Verifpal

A verifier is useful only when someone can model the relevant behavior, ask the right question and act on the answer. Verifpal treats the cost of those steps as a design problem. Its strongest case is the complete workflow it puts within reach of a protocol engineer.

A small language keeps attention on the protocol

Principals know values, generate nonces, compute and exchange messages. Five query forms cover specific confidentiality, authentication, freshness, equality and linkability checks. A reviewer can follow the model alongside a protocol description without first reading a process calculus or a formula over timepoints.

The 25 fixed primitives remove the task of defining their equations from each new model. That eliminates one opportunity for a modeling error and gives different models a shared vocabulary. It does not eliminate the need to choose an appropriate abstraction. Tamarin also supplies built-in theories; Verifpal’s distinctive choice is to require its fixed vocabulary throughout.

Assumptions can be inspected and changed

Guarded messages state authentic delivery. Checked operations state where a participant stops on failure. Phases place compromises in time, peer scenarios introduce different partners, and primitive annotations make weakened cryptography explicit. These features let a review ask concrete questions: what if this key arrives unauthenticated, the peer is malicious, or the long-term key leaks later?

// Fragment: Bob receives an authenticated key and checks the proof.
Alice -> Bob: [pk], proof
principal Bob[
	_ = SIGNVERIF(pk, challenge, proof)?
]

In the quickstart’s complete model, removing the brackets lets the attacker substitute its own key and signature. Removing ? lets Bob continue after a failed check. Small, reviewable edits connect a security result to the implementation requirement it depends on.

A bounded search still explores interactions between runs

The default expands each principal into two sessions that share long-term keys but generate distinct fresh values. The attacker can carry messages between those runs; peer scenarios also vary who the participants believe they are talking to. This reaches behavior that inspecting one honest execution would miss. The research paper demonstrates Lowe’s Needham–Schroeder relay, the FFGG rotation and attacks involving later key compromise. A finite analysis can expose consequential design errors even though it cannot establish that no other error exists.

A finding should explain what to investigate

Verifpal describes observations, constructions, substituted messages and checks using the names from the model. Session and scenario suffixes distinguish repeated runs. The intended reader is the person who wrote the exchange: they should be able to identify which key was trusted, which value was replaced and why the recipient accepted it.

This also helps audit the model. If a finding relies on observing a value that is encrypted in the real system, it points to an abstraction that needs repair. Readability matters on both sides of the analysis: discovering a protocol flaw and discovering that the analyst described the protocol incorrectly.

The analysis fits into ordinary development

The Workbench runs locally in a browser. Editor diagnostics, shareable models, structured reports and command-line checks support the same cycle outside it. A model and its expected findings can stay with a design as it changes. The value is the opportunity to ask more precise questions, earlier and more often.

Verifpal makes a compact modeling language and an understandable result the organizing priorities of the whole tool.

The work behind an unbounded proof

ProVerif and Tamarin do produce proofs of symbolic models, with a scope Verifpal does not provide. The practical question is how much work is needed to obtain that result for the protocol and property at hand.

TLS 1.3 with Tamarin: months of lemmas and substantial memory

Cremers et al.’s comprehensive analysis reports approximately three months of modeling work, most of it spent writing lemmas that divide the proof into manageable parts. With those lemmas, proving the entire model took about a week of work. Loading the model required over 10 GB of RAM, and a proof could consume 100 GB. Checking the completed proofs took about a day and still required substantial memory. The authors describe the manual guidance as part of constructing the proof, rather than merely running a verifier. A Comprehensive Symbolic Analysis of TLS 1.3, CCS 2017, §5.1.1.

5G authentication with Tamarin: building the automation

Basin et al.’s protocol model occupies roughly 500 lines. Its analysis uses 124 lemmas occupying about another 1,000 lines: helper lemmas, sanity checks and security claims, including variants that test which assumptions are necessary. Dedicated proof strategies add roughly 1,000 lines of Python; developing those strategies took several person-months. With that infrastructure in place, Tamarin established the proofs and found the attacks in about five hours.

The authors report that fully automatic mode without their proof strategies failed to establish relevant security properties and even full protocol executability. Their result demonstrates what expert-built automation can achieve, and makes its preparation cost explicit. A Formal Analysis of 5G Authentication, CCS 2018, §§4.4.2–4.4.3.

TLS 1.3 and TLS 1.2 with ProVerif: the cost of composition

Bhargavan, Blanchet and Kobeissi report that their individual TLS 1.3 and TLS 1.2 models verified in seconds, while composing them took several minutes. Adding features and modes increased both runtime and memory use; their scaling discussion reports hours on a powerful workstation for the final model combining all modes. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate, S&P 2017, §III.

The paper’s development summary separately reports 1,030 lines of ProVerif, about 70 minutes to complete its proof suite, and approximately three person-weeks for a ProVerif expert to develop the models. Fast individual checks and substantial overall analysis effort can coexist. Development effort, §VIII.

Those are ambitious historical case studies, not typical runtimes or a benchmark against Verifpal. They obtained much stronger guarantees than a bounded search, and both tools can finish simpler analyses automatically. They also helped evaluate evolving standards; proof tools are useful during design, too.

The case for Verifpal is that a team should be able to investigate protocol mistakes even when a proof development of that scale is outside its immediate resources. Finding a missing binding or an unjustified trust assumption is useful work in its own right. An unbounded proof remains a separate, stronger achievement when the project needs one.

What the results establish

All three tools analyze models. Their conclusions depend on the chosen algebra, attacker capabilities, protocol transcription and property. A proof of a model that aborts on an invalid signature does not cover code that continues after rejecting it. That shared limitation does not make a proof and a bounded search equivalent: with a faithful model, the proof rules out behavior that Verifpal may simply not have explored.

PASS [search exhausted at 2 sessions]

The implemented search found no contradiction at that session count, and its depth check rejected no proposal. It is not a proof even for all attacks at two sessions: the proposal and oracle families remain incomplete. Increasing the count explores more runs; --saturate observes agreement between successive result codes, not a theorem that later counts cannot differ.

PASS [search truncated: term depth]

No contradiction was found among the explored proposals, and a depth limit excluded at least one candidate. Preserve this qualification when reporting the result.

FAIL with a reproduced and grounded finding

The reduced state reproduces the query violation and the installed terms pass ordered derivability checks. This is stronger evidence than an unchecked solver proposal, but it is not a machine-checkable certificate of one compatible concurrent execution. Reports marked ungrounded or unreduced need further investigation; the paper classifies those categories as unconfirmed.

The results reference and the paper’s result-category table give the full scope. Keep the model, version, assumptions, bounds and witness qualifications with any finding. Reproduce the behavior against the implementation when making a claim about a deployed system.

Property names also need care. Verifpal’s equivalence? compares resolved values; it does not establish observational equivalence. Its unlinkability? searches for a concrete link witness, rather than proving that two executions are indistinguishable. Its use-based authentication checks are not interchangeable with arbitrary completion correspondences. ProVerif and Tamarin support richer properties, including equivalence analyses whose sufficient conditions can themselves be stronger than the privacy property you intended. See the ProVerif property guide and Tamarin’s equivalence documentation.

At a glance

Choosing a tool

Start with whether the tool can faithfully express your protocol and the property you need. A convenient model that omits a decisive algebraic behavior cannot answer the original question.

• Choose Verifpal for an accessible cycle of modeling, bounded attack search and design review when the fixed primitives and query meanings fit. It is particularly useful when protocol authors need to read and challenge the analysis themselves.
• Choose ProVerif when you need automated unbounded proofs and your protocol, equations and properties fit its process model and abstraction. Be prepared to investigate inconclusive results or refine difficult models.
• Choose Tamarin when explicit mutable state, richer algebra or flexible temporal properties are central, and you need unbounded reasoning with the option to guide proofs interactively.

These choices can be combined. A small Verifpal model can expose design mistakes and clarify assumptions before a more expressive model addresses stronger claims. Translating between tools still requires aligning the threat model and the exact property; matching verdict labels alone is not a cross-check.

Verifpal earns its place by making rigorous questions easier to ask and findings easier to use. The goal is for more of the people building a protocol to participate in its analysis, and for that analysis to improve the design while changes are still practical.