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