Cryptology ePrint Archive: Report 2007/199

A Framework for Game-Based Security Proofs

David Nowak

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.

Category / Keywords: foundations / sequence of games, proof assistant, formal verification, monad, probability

Publication Info: A short version of this paper will appear in the proceedings of ICICS 2007

Date: received 28 May 2007, last revised 7 Nov 2007

Contact author: david nowak at aist go jp

Available format(s): PDF | BibTeX Citation

Note: The source code is available at:

28 May 2007: first public version

22 Jun 2007: added application to the hashed version of the encryption scheme ElGamal

1 Oct 2007: short version accepted at ICICS 2007:

7 Nov 2007: added more explanations following comments by anonymous reviewers

Version: 20071107:103035 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]