Events & Talks
Eurocrypt 2022 Affiliated Event
Thank you, workshop attendees!
The Verifpal workshop at Eurocrypt 2022 was a success. Please feel free to download the slides in PDF format, and to contact me via email with any follow-up questions!
What is Verifpal?
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.
Why should I attend this workshop?
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!
Modeling and analyzing cryptographic protocols has become an essential aspect of the applied cryptographer toolkit thanks to major advances in state-of-the-art modeling and analysis tools such as Tamarin and ProVerif, used to analyze, improve and find attacks in TLS, 5G, the Noise Protocol Framework, Signal, and much more.
However, these analysis tools often obtain their strength and comprehensive featureset at the inevitable expense of a complex domain-specific language with steep learning curve. Verifpal goes the opposite direction: excel in being easy to use, even if that means less soundness.
Since its introduction in 2019, Verifpal has best positioned itself as a great introduction to the world of cryptographic protocol modeling, analysis and verification, with the aim of being an inclusive and pedagogical stepping stone for students, onto more complex frameworks.
At the Verifpal tutorial, we first begin by using Verifpal to teach the basics of protocol modeling through Verifpal's intuitive syntax, which lets you express, reason about, model and analyze protocol ideas more quickly than other tools.
We then move onto the second part, in which we use what we've learned through Verifpal to introduce Tamarin, ProVerif, CryptoVerif, and F*, explaining how they all work, their differences and relative strengths.
The Verifpal Tutorial at Eurocrypt 2022 is meant to be a comprehensive introduction to the world of formal protocol modeling, that manages to be inclusive and accessible even if you're a student just starting out with little (or no) background in formal methods!
Provisional Program
The workshop will be held on Sunday, May 29th, 2022 at the Clarion Hotel Trondheim (the main Eurocrypt 2022 venue) in conference room Cosmos 3A. Please do your best to arrive on time.
- 09:00—09:45 💻Introduction and Software Setup
- 09:45—10:30 📖Learning the Language with Examples
- 10:30—10:50 ☕Coffee Break
- 10:50—12:30 📖Modeling Signal in Verifpal
- 12:30—14:00 🍱Lunch Break
- 14:00—15:30 📖A Look at ProVerif and Tamarin
- 15:30—16:00 ☕Coffee Break
- 16:00—17:30 📖A Look at CryptoVerif and F*
- 17:30—18:00 🙋Questions and Answers, Discussion
Attending the Verifpal Tutorial
The Verifpal Tutorial will be held in conjunction with Eurocrypt 2022 on Sunday, May 29th, 2022, at the main Eurocrypt 2022 venue (Clarion Hotel Trondheim). Eurocrypt 2022 is organized by the International Association for Cryptologic Research (IACR) and the Verifpal Tutorial will be carried out under the Eurocrypt 2022 Code of Conduct.
Important Attendance Links
- Register to Eurocrypt 2022 and select “Verifpal Tutorial” as your affiliated event option for Sunday, May 29th, 2022.
- Subscribe to the Verifpal Tutorial newsletter to receive important announcements, including when Eurocrypt 2022 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.
The Verifpal User Manual is available for download as a PDF.
Required Materials
Attendees are expected to bring one laptop computer each, with the following capabilities:
- Running the Windows, Linux, macOS or FreeBSD operating system.
- Connecting to the Internet via Wi-Fi.
- Installing software from the Internet.
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; we will do our best such that the success of your learning experience is guaranteed!
Organizing Committee
- Nadim Kobeissi, Symbolic Software: Verifpal author.
- Georgio Nicolas, KU Leuven COSIC Group: Verifpal contributor.
