Verifpal

Security Verification for Cryptographic Protocols: A Workshop Organized at the American University of Beirut

Cryptographic protocols, such as Signal (used in WhatsApp) and TLS 1.3 (used in HTTPS/all web browsers) are responsible for much of the security that we rely on in our daily Internet communications.

It is only thanks to the intricate design of these cryptographic systems that our WhatsApp conversations remain confidential even from WhatsApp employees, or that our Gmail login remain protected against interception even from our own Internet Service Provider (ISP).

But how are these systems designed? What sort of cryptographic components are used? And once we have a full protocol, how can we verify that it actually achieves the guarantees that we expect?

Formal Verification is a technique that can help us answer these questions. Using automated formal verification software, we can write models representing the cryptographic protocols that we would like to investigate. Then, we can posit queries and understand whether these queries are satisfied by our model. These queries can be questions such as: does WhatsApp's encryption protocol really keep Alice and Bob's messages confidential? And what is it that prevents Alice from impersonating Carol when talking to Bob?

At the Verifpal Workshop, 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

The workshop will be held at the American University of Beirut campus on Saturday, November 30th, 2019, in room IOEC 518.

  • 1:00PM: Wait for inevitably late student.
  • 1:10PM: Overview of modern cryptographic protocols and primitives.
  • 2:00PM: Overview of formal verification technologies + Verifpal setup.
  • 2:30PM: Modeling Signal Protocol in Verifpal.
  • 3:15PM: 15 minute break.
  • 3:30PM: Modeling TLS 1.3 in Verifpal.
  • 4:30PM: Looking at ProVerif and CryptoVerif.

Requirements

Your focus is appreciated at all times. Please also bring:

  • A laptop computer running Windows, Linux or macOS.
  • Access to an Internet connection (AUB, tethering, etc.)

Expected Results

At the end of this workshop, you will have learned:

  • How to reason about the design of modern cryptographic protocols.
  • A basic overview of the landscape of modern formal verification technologies.
  • How to use Verifpal and ProVerif.

© 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.

HTML5 Valid