4pm - 5pm
Thursday 29 April 2021
State-Separating Proofs as Sketches for Machine-Checked Cryptographic Proofs
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  and proofs  are available, although the talk will go beyond them.
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
Find your local number.
- +44 203 481 5237 United Kingdom
- +44 203 481 5240 United Kingdom
- +44 203 901 7895 United Kingdom
- +44 208 080 6591 United Kingdom
- +44 208 080 6592 United Kingdom
- +44 330 088 5830 United Kingdom
- +44 131 460 1196 United Kingdom
+442034815237,,92154194306#,,,,*163426# United Kingdom
+442034815240,,92154194306#,,,,*163426# United Kingdom