10 Jul 2014 - Myrto Arapinis

V. Shoup, Sequences of Games: A tool for Taming Complexity in Security Proofs

Abstract

Security proofs in cryptography may sometimes be organized as sequences of games. In certain circumstances, this can be a useful tool in taming the complexity of security proofs that might otherwise become so messy, complicated, and subtle as to be nearly impossible to verify. This technique appears in the literature in various styles, and with various degrees of rigor and formality. This paper is meant to serve as a brief tutorial on one particular “style” of employing this technique, which seems to achieve a reasonable level of mathematical rigor and clarity, while not getting bogged down with too much formalism or overly restrictive rules. We do not make any particular claims of originality - it is simply hoped that others might profit from some of the ideas discussed here in reasoning about security.

At the outset, it should be noted that this technique is certainly not applicable to all security proofs. Moreover, even when this technique is applicable, it is only a tool for organizing a proof — the actual ideas for a cryptographic construction and security analysis must come from elsewhere.