CryptoDB
A Framework for Game-Based Security Proofs
| Authors: | |
|---|---|
| Download: | |
| 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
}