4pm - 5pm

Thursday 29 April 2021

State-Separating Proofs as Sketches for Machine-Checked Cryptographic Proofs


back to all events

This event has passed

There is no need to register, just login to the Zoom call on the day.


The last decade has seen significant progress in the development of techniques and tools for machine-checking cryptographic proofs. Out of the challenges such formalisation efforts pose at even medium scale, new pen-and-paper techniques that mimic the techniques without the formality imposed by the tools have arisen, and are now seeing use in some cryptographic communities. In this talk, I will discuss how one such proof technique—state-separating proofs—can in fact be used to guide the formal development of proofs in existing tools (here, EasyCrypt) _without_ giving them formal semantics. In particular, although state-separating proofs are designed to compose well, we do not explicitly formalise generic composition results, instead relying on the composition properties of EasyCrypt modules and proofs. This enables us to mix-and-match state-separation and more traditional security definitions, depending on the component under study.

This is work-in-progress with Konrad Kohbrok (then Aalto University, now at Wire) and Sabine Oechsner (Aarhus University). Preliminary results [0] and proofs [1] are available, although the talk will go beyond them.

[0]: https://eprint.iacr.org/2021/326
[1]: https://gitlab.com/fdupress/ec-cryptobox


François Dupressoir will be speaking at this event.

How to attend

This will be an online event held on Zoom.

  • Meeting ID: 921 5419 43061
  • Passcode: 163426

Attend the seminar

Visitor information

Find out how to get to the University, make your way around campus and see what you can do when you get here.