With Verifpal, everyone can learn how to model and verify cryptographic protocols!
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 is available as free and open source software.
By supporting Verifpal, you will be helping us:
- Improve Verifpal's soundness with a full proof of soundness and a full automated test suite.
- Allow Verifpal to generate implementations in Go from models, thanks to sound verification methodology.
- Expand Verifpal's IDE integration: live analysis feedback and charts as protocol is modeled in Visual Studio Code.
- Have more time for bug fixes, general improvements, etc.
- Implement support for more types of verification queries: forward secrecy, etc.
- Expand the language's features as requested already by community members on the Verifpal Mailing List.
- Improve packaging and distribution.
You would also be supporting our initiative to get Verifpal taught at the undergraduate level. Verifpal is already being taught this semester in a computer security course at NYU, and 50 hardcover copies of the Verifpal User Manual have been printed for use as textbooks. We plan to expand this initiative to leverage Verifpal as an educational tool for computer security and correct protocol design.
verifpal joined 3 years ago.