This seminar has passed.

EasyCrypt in anger — Proofs for Primitives, Constructions and Protocols

March 22 (2023) @ 3:00 pm - 4:00 pm

Abstract: The EasyCrypt proof assistant offers—in a single tool—the ability to reason about cryptographic security at various scales from primitives to protocols. However, this flexibility comes at a huge cost in usability. This talk will discuss insights gained through the recent formalisation of primitives (SHA-3, XMSS), constructions (KMS, crypto_box) and protocols (distance-bounding, AKE) and explore plans for improvements to the tool that would enable its use on larger protocols, and for the creation of beginner-friendly tutorial material that would enable it to be used more broadly.

This is a joint seminar with FM-SEC.

Attendance via Zoom (ID: 968 7078 6660, Passcode: 081732)

Livestream via YouTube

Details

Date:: March 22 (2023)
Time:: 3:00 pm - 4:00 pm
Seminar Tags:: Cryptography, EasyCrypt, formal analysis

Presenter

: François Dupressoir (University of Bristol)

François Dupressoir is a Senior Lecturer in Cryptography at the University of Bristol, where he also serves as Head of the Cryptography Research Group. He has been a member of the EasyCrypt development team since he got his PhD in 2012, first at the IMDEA Software Institute, then at the University of Surrey, and finally at Bristol; with a focus on using formal methods to improve the real-world security of cryptographic systems.