International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Paper: A Framework for Game-Based Security Proofs

Authors:
David Nowak
Download:
URL: http://eprint.iacr.org/2007/199
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.
BibTeX
@misc{eprint-2007-13480,
  title={A Framework for Game-Based Security Proofs},
  booktitle={IACR Eprint archive},
  keywords={foundations / sequence of games, proof assistant, formal verification, monad, probability},
  url={http://eprint.iacr.org/2007/199},
  note={A short version of this paper will appear in the proceedings of ICICS 2007 david.nowak@aist.go.jp 13824 received 28 May 2007, last revised 7 Nov 2007},
  author={David Nowak},
  year=2007
}