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 . 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.
 Victor Shoup: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004: 332 (2004)
 Mihir Bellare, Phillip Rogaway: The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. EUROCRYPT 2006
 Chris Brzuska, Antoine Delignat-Lavaud, Cedric Fournet, Konrad Kohbrok, Markulf Kohlweiss: State Separation for Code-Based Game-Playing Proofs. ASIACRYPT 2018
Last update: 2020-01-23