Paper 2018/306

State Separation for Code-Based Game-Playing Proofs

Chris Brzuska, Aalto University
Antoine Delignat-Lavaud, Microsoft Research (United Kingdom)
Cedric Fournet, Microsoft Research (United Kingdom)
Konrad Kohbrok, Aalto University
Markulf Kohlweiss, University of Edinburgh

The security analysis of real-world protocols involves reduction steps that are conceptually simple but still have to account for many protocol complications found in standards and implementations. Taking inspiration from universal composability, abstract cryptography, process algebras, and type-based verification frameworks, we propose a method to simplify large reductions, avoid mistakes in carrying them out, and obtain concise security statements. Our method decomposes monolithic games into collections of stateful *packages* representing collections of oracles that call one another using well-defined interfaces. Every component scheme yields a pair of a real and an ideal package. In security proofs, we then successively replace each real package with its ideal counterpart, treating the other packages as the reduction. We build this reduction by applying a number of algebraic operations on packages justified by their state separation. Our method handles reductions that emulate the game perfectly, and leaves more complex arguments to existing game-based proof techniques such as the code-based analysis suggested by Bellare and Rogaway. It also facilitates computer-aided proofs, inasmuch as the perfect reductions steps can be automatically discharged by proof assistants. We illustrate our method on two generic composition proofs: (1) a proof of self-composition using a hybrid argument; and (2) the composition of keying and keyed components. For concreteness, we apply them to the KEM-DEM proof of hybrid-encryption by Cramer and Shoup and to the composition of forward-secure game-based key exchange protocols with symmetric-key protocols.

Note: This revision adds a discussion of follow-up work and treats the absolute values in the hybrid argument in Appendix B in a clean way. We thank Lúcás Críostóir Meier for pointing out that they weren't handled properly.

Available format(s)
Publication info
A major revision of an IACR publication in ASIACRYPT 2018
compositionverificationkey exchangeKEM-DEM
Contact author(s)
chris brzuska @ gmail com
antdl @ microsoft com
fournet @ microsoft com
konrad kohbrok @ datashrine de
mkohlwei @ ed ac uk
2023-06-08: last of 3 revisions
2018-04-03: received
See all versions
Short URL
Creative Commons Attribution


      author = {Chris Brzuska and Antoine Delignat-Lavaud and Cedric Fournet and Konrad Kohbrok and Markulf Kohlweiss},
      title = {State Separation for Code-Based Game-Playing Proofs},
      howpublished = {Cryptology ePrint Archive, Paper 2018/306},
      year = {2018},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.