Paper 2018/306

State-Separating Proofs: A Reduction Methodology for Real-World Protocols

Chris Brzuska and Antoine Delignat-Lavaud and Konrad Kohbrok and Markulf Kohlweiss

Abstract

The security analysis of real-world protocols involves reduction steps that are conceptually simple but have to handle complicated protocol details. Taking inspiration from Universal Composability, Abstract Cryptography, Pi-calculus and F*-based analysis we propose a new technique for writing simple reductions to avoid mistakes, have more selfcontained concrete security statements, and allow the writer and reader to focus on the interesting steps of the proof. Our method replaces a monolithic protocol game with a collection of so-called packages that are composed by calling each other. Every component scheme is replaced by a package parameterized by a bit b. Packages with a bit 0 behave like a concrete scheme, while packages with a bit 1 behave like an ideal version. The indistinguishability of the two packages captures security properties, such as the concrete pseudo-random function being indistinguishable from a random function. In a security proof of a real-life protocol, one then needs to flip a package’s bit from 0 to 1. To do so, in our methodology, we consider all other packages as the reduction. We facilitate the concise description of such reductions by a number of Pi-calculus-style algebraic operations on packages that are justified by state separation and interface restrictions. Our proof method handles “simple” steps using algebraic rules and leaves “interesting” steps to existing game-based proof techniques such as, e.g., the code-based analysis suggested by Bellare and Rogaway. In addition to making simple reductions more precise, we apply our techniques to two composition proofs: a proof of self-composition using a hybrid argument, and the composition of key generating and key consuming components. Consistent with our algebraic style the proofs are generic. For concreteness, we apply them to the KEM-DEM proof of hybrid-encryption by Cramer and Shoup and the proof for composability of Bellare-Rogaway secure key exchange protocols with symmetric-key protocols.