Events & Talks

Eurocrypt 2021 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.

IACR logo

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!

Program

  • 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 📖Modeling TLS 1.3 in Verifpal
  • 15:30—16:00 ☕Coffee Break
  • 16:00—17:30 📖A Look at ProVerif, Tamarin, 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 2021 on Saturday, October 16th 2021 at the To Be Determined. Eurocrypt 2021 is organized by the International Association for Cryptologic Research (IACR) and the Verifpal Tutorial will be carried out under the Eurocrypt 2021 Code of Conduct.

Important Attendance Links

  • Register to Eurocrypt 2021 and select “Verifpal Tutorial” as your affiliated event option for Saturday, October 16, 2021.
  • Subscribe to the Verifpal Tutorial newsletter to receive important announcements, including when Eurocrypt 2021 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

© Copyright 2019- Nadim Kobeissi. All Rights Reserved. “Verifpal” and the “Verifpal” logo/mascot are registered trademarks of Nadim Kobeissi. Verifpal software is provided as free and open source software, licensed under the GPLv3. Verifpal User Manual, as well as this website, are provided under the CC BY-NC-ND 4.0 license. Published by Symbolic Software.