Resources for Writing Security Proofs
This brief post collects resources and tutorials that I found helpful when learning and teaching how to write security proofs. The main tools are security reductions and game-hopping. I list resources for each of them and then expand on what I found useful in each.
Security Reductions
- Katz and Lindell, Introduction to Modern Cryptography, Chapter 3.1.3.
- Boneh and Shoup, A Graduate Course in Applied Cryptography, Section 2.2.3.1.
Security reductions are the basic building block of security proofs. The idea is to show that breaking a protocol $\Pi$ is at least as hard as breaking some underlying assumption or protocol $\Pi’$. I like the introduction given in Introduction to Modern Cryptography by Katz and Lindell in Chapter 3.1.3, p. 58.
There are plenty of examples of such proofs in A Graduate Course in Applied Cryptography by Boneh and Shoup. The first one being in Section 2.2.3.1 “Message recovery attacks”.
Games and Game-Hopping
- Shoup, Sequences of games: a tool for taming complexity in security proofs.
- Boneh and Shoup, A Graduate Course in Applied Cryptography, Section 3.11.
- Fischlin and Mittelbach, An Overview of the Hybrid Argument, Section 3.
Complex protocols rely on more than one assumption or underlying primitives. In such cases, a single reduction will not be enough to give a full security analysis. Instead we want to use a strategy known as “game-hopping” or “sequence of games”. This technique is used in most papers but is rarely taught explicitly.
Shoup’s game-hopping. The first rigorous and manageable explanation of the technique that I found was Victor Shoup’s tutorial on “Sequences of games: a tool for taming complexity in security proofs”. The framework is formal enough that we won’t be writing broken proofs but at the same time is not too restrictive and preserves intuition. I also like that it gives names to three types of common game hops:
- transitions based on indistinguishability.
- transitions based on failure events.
- bridging steps.
Section 1.2 also sheds some light on the term “hybrid argument” which seems to pop up in many papers but can be quite mystical if not explained properly. In particular, he explains that they are a special case of the “sequence of games” strategy where all hops are transitions based on indistinguishability.
“Hybrid” arguments. Since I mention hybrid arguments, I didn’t get my “A-HA” moment from Shoup’s manuscript. For me it came in two steps. The first was understanding what indistinguishability games are from Boneh and Shoup; the second was the example applications of a hybrid argument given in Section 3 of “An Overview of the Hybrid Argument” by Fischlin and Mittelbach.
Proofs IRL
In practice, the above techniques are used in different styles. For example, in the SNARG book (Chiesa and Yogev, Building Cryptographic Proofs from Hash Functions), the authors prefer to define “probabilistic experiments” and write proofs by analyzing the corresponding probabilities. These could have also been cast as games; it’s a matter of taste and convenience.
You will also find that authors often skip steps e.g., “this can be shown using a simple [reduction / hybrid argument]” or “if event A happens, we have found a collision in the hash function”. The latter sentence is in fact a transition based on a failure event and a reduction from the failure event to the collision-finding game. However, since both of these are so standard, we tend to save space and spare the reader from unnecessary reading and formalism.