CAPS
Workshop on Computer-Aided Proofs of Security - Sunday May 4th 2025
Interested in this formal verification thing everyone talks about, but no clue where to start? EasyCrypt, ProVerif, Lean, aren't they all the same? Why are there so many tools when one should be enough? CAPS will give you an overview of the formal verification tool landscape for cryptographic security, for primitives and protocols, and from symbolic to computational security and everything in between.
The workshop's aim is to give cryptographers an overview of the current tool landscape around cryptographic security proofs, from the perspective of how they would interact with the tools. More generally, we hope to bring together researchers and practitioners in cryptography and formal methods that are interested in computer-aided security proofs.
Program
| 9:00-9:30 | Workshop Introduction and Security Overview by the organizers |
| 9:30-9:45 | Primitives: KEM-DEM Security Pen & Paper Proof |
| 9:45-10:30 | KEM-DEM & more in ProofFrog by Douglas Stebila |
| 10:30-11:00 | coffee break |
| 11:00-12:00 | KEM-DEM & more in EasyCrypt by François Dupressoir |
| 12:00-12:15 | Protocols: Key Exchange Security Pen & Paper Proof by Doreen Riepel |
| 12:15-13:00 | Key Exchange & more in ProVerif by Vincent Cheval |
| 13:00-14:15 | lunch break |
| 14:15-15:00 | Key Exchange & more in Tamarin by Cas Cremers |
| 15:00-15:45 | coffee break |
| 15:45-17:15 | Round Table with Tool Developers: The State of Computer-Aided Proofs of Security |
(Subject to change)
Date and Location
Date: Sunday, May 4th, 2025
Location: Facultad de Ciencias Matemáticas, Universidad Complutense de Madrid (UCM)in Madrid, Spain. (Room TBD.)
The venue is near the Ciudad Universitaria (line 6) metro stop.
Registration
Please register through the Eurocrypt 2025 website by selecting CAPS as your "workshop day 2" event.
Related Events
CAPS'25 will be held in Madrid, Spain, on Sunday, May 4th, as a Eurocrypt 2025 affiliated event. Please register through the Eurocrypt 2025 website by selecting CAPS as your "workshop day 2" event.
If you are excited about CAPS, the ProTeCS workshop may also interest you. It provides a less verification-focused take on cryptographic proofs on the day before CAPS.
Resources
- Material presented in the talks: to be added after the workshop.
- List of Verification Projects curated by the High-Assurance Cryptographic Software Workshop
Organizers
- Deirdre Connolly, SandboxAQ
- Philipp Haselwarter, Aarhus University
- Sabine Oechsner, Vrije Universiteit Amsterdam
Last updated April 15, 2025