International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: A Framework for Game-Based Security Proofs

David Nowak
Search ePrint
Search Google
Abstract: Information security is nowadays an important issue. Its essential ingredient is cryptography. A common way to present security proofs is to structure them as sequences of games. The main contribution of this paper is a framework which refines this approach. We make explicit important theorems used implicitly by cryptographers but never explicitly stated. Our aim is to have a framework in which proofs are precise enough to be mechanically checked, and readable enough to be humanly checked. We illustrate the use of our framework by proving in a systematic way the so-called semantic security of the encryption scheme ElGamal and its hashed version. All proofs have been mechanically checked in the proof assistant Coq.
  title={A Framework for Game-Based Security Proofs},
  booktitle={IACR Eprint archive},
  keywords={foundations / sequence of games, proof assistant, formal verification, monad, probability},
  note={A short version of this paper will appear in the proceedings of ICICS 2007 13824 received 28 May 2007, last revised 7 Nov 2007},
  author={David Nowak},