Verifpal

Verifpal is software for verifying the security of cryptographic protocols. It comes out of the same symbolic verification tradition as ProVerif and Tamarin, but is written for practitioners and students rather than for specialists.

You describe a protocol roughly the way you would describe it out loud, and the description is still precise enough to analyze. Primitives are built in rather than user-defined, which removes a common source of modeling error. The attacker is active: it reads the network and tampers with anything you have not explicitly guarded. Queries cover forward secrecy, key compromise impersonation and other properties that depend on fresh values.

Every principal runs two concurrent sessions by default, so you get cross-session attacks (a nonce swapped between two instances of a role, a message replayed from one session into another) without duplicating principals by hand. Set the count with verifpal verify model.vp --sessions k.

When a query is contradicted, Verifpal minimizes the attack and then narrates what remains as numbered causal steps, using the names your model gave the values. If the analysis ran under declared weakening assumptions, or the search declined a branch, the output says so.

verifpal verify model.vp --format html > report.html renders the whole analysis as a single self-contained HTML page — verdicts, attack traces each drawn as a sequence diagram with the attacker's lane, an annotated protocol diagram, and the syntax-highlighted model source with each query marked by its verdict — with no external resources, so it opens identically offline and can be attached to a review or mailed to a colleague. --format json emits the same report as machine-readable JSON, including the structured attack steps. --format tex emits it as a LaTeX document that compiles with tectonic as it stands, typesetting terms as mathematics and every attack as a keyed message-sequence chart beside its numbered trace — each figure delimited by comment markers and built from one preamble block, so a diagram can be lifted straight into a paper.

Verifpal has been used to verify security properties for Signal, Scuttlebutt, TLS 1.3, Telegram and other protocols.

Scientific Paper

From Toy to Instrument: Seven Years of Verifpal documents the semantics, the deduction rules, the search, the witness-transfer theorem, the termination bound and the session model, along with what each of them does not cover.

Validation and Search Bounds

The solver proposes substitutions. Independent validation checks attacker control, derivability, causal availability and compatible execution constraints before re-execution. Every reported attack must also reproduce and pass grounding from baseline knowledge. The paper states the additional support condition under which a reproduced witness transfers to a single protocol history.

A passing query means "this search found no attack", which is weaker than a proof. Verifpal supports neither observational equivalence nor user-defined equational theories, and it always terminates instead of offering unbounded session replication. If you are designing a protocol for production, cross-check it with ProVerif and Tamarin.

Getting Started

Read the Verifpal Documentation first.

On Windows, install through Scoop:

scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git
scoop install verifpal

On Linux and macOS, install through Homebrew:

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

Both give you automatic updates. Otherwise, grab a release for Windows, Linux or macOS, or build from source.

Building from Source

With Rust installed, cargo build --release produces the binary under target/release/. cargo test --release runs the full test suite.

Editor Support

Verifpal ships a language server (verifpal lsp), and the project maintains an extension for each of these editors on top of it:

• Visual Studio Code (source): syntax highlighting, automatic formatting, live query analysis and protocol diagrams as you write the model. Search for "Verifpal" from inside Visual Studio Code to install it.
• Neovim: syntax highlighting, verification diagnostics on each query line, formatting and hover documentation.
• Zed: syntax highlighting, live error checking and attacker analysis.

License

Verifpal and its editor extensions are published by Symbolic Software as free and open source software under the GNU General Public License, version 3. The Verifpal User Manual is provided under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) license.

© Copyright 2019-2026 Nadim Kobeissi. All Rights Reserved. “Verifpal” and the “Verifpal” logo/mascot are registered trademarks of Nadim Kobeissi.