WoDUP, May 9, 2020, Zagreb, Croatia
Workshop on developing, using and teaching cryptographic proofs

Cryptographers who joined the field after ca. 2000 have received significant guidance by the community in how to determine good security definitions: A definition needs to (1) have a clear conceptual motivation, (2) have a clear description, (3) come with a discussion of necessary, arbitrary and convenient choices as well as (4) a discussion of advantages/disadvantages compared to existing definitions. The community effort to provide similar guidance for proofs is ongoing, and this Tutorial on Reduction Proofs is a part of it. We aim to share our own insights on how we write and structure security proofs, hoping to break down some of the access barriers of the field and, hopefully, providing inspiration also to experienced theorem provers as well as lecturers.

In the morning, we present reductions for several classic game-hopping proofs exposed in a way that we find personally insightful, inspired by ideas of code-based game-playing [1,2] and state-separating proofs [3]. We then apply game-hopping ideas to simulation-based security and give as an example a modular security proof of Yao's Garbled Circuits. In particular, the proof exploits the ability to define subgames of large security experiments and to compose the derived security statements. In the afternoon, we explain how to write structured key exchange proofs on the example of SHS2, a protocol developed and used by the peer-to-peer community Scuttlebutt. We then turn to the mammoth task of developing a proof for the TLS 1.3 Handshake protocol which, again, uses subgames and composable security statements in an essential way. The perspective adopted by WoDUP throughout all examples is proof-based, meaning that we compose the derived security statements. We thus add (5) easy to deploy in proofs, to the above guidelines for good security definitions. Finally, we turn to discussing how to teach (reduction-based) cryptography in university settings.

[1] Victor Shoup: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004: 332 (2004)

[2] Mihir Bellare, Phillip Rogaway: The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. EUROCRYPT 2006

[3] Chris Brzuska, Antoine Delignat-Lavaud, Cedric Fournet, Konrad Kohbrok, Markulf Kohlweiss: State Separation for Code-Based Game-Playing Proofs. ASIACRYPT 2018


Organizors: Chris Brzuska (Aalto University), Markulf Kohlweiss (Edinburgh University), Sabine Oechsner (Aarhus University)

Location: WoDUP is a Eurocrypt 2020 Affiliated Event. For location, see Eurocrypt Webpage

Registration: As WoDUP is a Eurocrypt 2020 Affiliated Event, registration is part of rhr Eurocrypt Affiliated Events Registration (there is no separate registration only for the WADUP workshop).

Return to Chris Brzuska's Homepage

Last update: 2020-01-23