Verifpal

IACR logo

Eurocrypt 2020 Affiliated Event

The security of cryptographic protocols remains as relevant as ever, with systems such as TLS and Signal being responsible for much of the Web’s security guarantees. One main venue for the analysis and verification of these protocols has been automated analysis with formal verification tools, such as ProVerif, CryptoVerif and Tamarin. Indeed, these tools have led to confirming security guarantees (as well as finding attacks) in secure channel protocols, including TLS and Signal. However, formal verification in general has not managed to significantly attract a wider audience.

Verifpal is new software for verifying the security of cryptographic protocols that aims is to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 and other protocols. It is a community-focused project, and available under a GPLv3 license.

At the Verifpal Tutorial, you will learn...

...how to use Verifpal to model and verify the security goals of advanced, cutting-edge protocols such as Signal and TLS 1.3. No prior knowledge in formal verification is necessary — Verifpal is specifically tailored for beginners and newcomers!

Attending the Verifpal Tutorial

The Verifpal Tutorial will be held in conjunction with Eurocrypt 2020 in Zagreb, Croatia, on Saturday, May 9, 2020 at The Westin Zagreb Hotel. Eurocrypt 2020 is organized by the International Association for Cryptologic Research (IACR) and the Verifpal Tutorial will be carried out under the Eurocrypt 2020 Code of Conduct.

Important attendance links:
  • Register to Eurocrypt 2020 and select “Verifpal Tutorial” as your affiliated event option for Saturday, May 9 2020.
  • Subscribe to the Verifpal Tutorial newsletter to receive important announcements, including when Eurocrypt 2020 registration will open and the finalized information (conference room, etc.) regarding the tutorial.
  • Optionally, consider subscribing to the main Verifpal Mailing List to participate in more general news and discussion regarding Verifpal.

High quality, hardcover, full-color copies of the Verifpal User Manual will be available for purchase at the event for €15 (with a Verifpal Sticker Pack inside!) The Verifpal User Manual is also available for download as a PDF.

Tutorial Schedule

  • 09:00 Introduction to Verifpal and Software Setup
  • 10:00 Learning the Language with Examples
  • 12:00 Coffee Break
  • 12:30 Modeling Signal in Verifpal
  • 14:00 Modeling TLS 1.3 in Verifpal
  • 15:00 Questions and Answers
  • 15:30 Tutorial Conclusion

Expected Audience

Given Verifpal’s focus on ease of use, pedagogy and accessibility, the goal is to attract the most diverse possible audience to the tutorial. Each participant will be attended to personally by the organizer.

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.

Sponsors


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.

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