Verifpal

Verifpal is new software for verifying the security of cryptographic protocols. Building upon contemporary research in symbolic formal verification, Verifpal’s main aim is to appeal more to real-world practitioners, students and engineers without sacrificing comprehensive formal verification features.

In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is much easier to write and understand than the languages employed by existing tools. At the same time, Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation.

Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3, Telegram and other protocols. It is a community-focused project, and available under a GPLv3 license.

An Intuitive Protocol Modeling Language

The Verifpal language is meant to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling. Verifpal reasons about the protocol model with explicit principals: Alice and Bob exist and have independent states.

Modeling that Avoids User Error

Verifpal does not allow users to define their own cryptographic primitives. Instead, it comes with built-in cryptographic functions — this is meant to remove the potential for users to define fundamental cryptographic operations incorrectly.

Easy to Understand Analysis Output

When a contradiction is found for a query, the result is related in a readable format that ties the attack to a real-world scenario. This is done by using terminology to indicate how the attack could have been possible, such as through a man-in-the-middle on ephemeral keys.

Friendly and Integrated Software

Verifpal comes with a Visual Studio Code extension that offers syntax highlighting and, soon, live query verification within Visual Studio Code, allowing developers to obtain insights on their model as they are writing it.

Download Verifpal

Verifpal is available for Windows, Linux and macOS. The Verifpal User Manual is an essential guide to getting started with cryptographic protocol analysis using Verifpal: please click the User Manual cover to download your copy.

Verifpal is free and open source software. Source code is available on the 💾Verifpal Source Repository.

On Linux and macOS, quick (and less safe) installation is possible by running:
bash -c "curl -sL https://verifpal.com/install|bash"


About the Project

Verifpal is Experimental Software

Verifpal is still highly experimental software. Using it in a classroom or learning environment is welcome, but it should not yet be relied upon for academic formal verification work. For that, check out ProVerif.

News and Discussion

Sign up to the 📧Verifpal Mailing List to stay informed on the latest news and announcements regarding Verifpal, and to participate in Verifpal discussions.

Scientific Background

A 📄Verifpal Scientific Paper is available for those interested in the project’s technical and research motivations.

Verifpal is inspired by the two decades of seminal work on formal verification by Prof. Bruno Blanchet, the author of the ProVerif formal verification software.

Stickers and Wallpapers

Show your support for Verifpal with a cool sticker from the 🛍️Verifpal Sticker Shop, or by downloading a nice Verifpal wallpaper (A, B) for your desktop!

Sponsors and Donations


Verifpal is sponsored by the NLNet Foundation. Funding was provided through the NGI0 Privacy Enhancing Technologies Fund, a fund established by NLnet with financial support from the European Commission’s Next Generation Internet program, under the aegis of DG Communications Networks, Content and Technology under grant agreement №825310.

Donate to Support Verifpal!

Verifpal is free and open source software, and every donation will be used to continue Verifpal research and development. If you're interested in supporting Verifpal, please consider setting up a recurring or one-time donation today!

License

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

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