Sciweavers

Share
TYPES
2004
Springer

A Machine-Checked Formalization of the Random Oracle Model

8 years 8 months ago
A Machine-Checked Formalization of the Random Oracle Model
Abstract. Most approaches to the formal analysis of cryptography protocols make the perfect cryptographic assumption, which entails for example that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. Ideally, one would prefer to abandon the perfect cryptography hypothesis and reason about the computational cost of breaking a cryptographic scheme by achieving such goals as gaining information about the plaintext pertaining to a ciphertext without knowing the key. Such a view is permitted by non-standard computational models such as the Generic Model and the Random Oracle Model. Using the proof assistant Coq, we provide a machine-checked account of the Generic Model and the Random Oracle Model. We exploit this framework to prove the security of the ElGamal cryptosystem against adaptive chosen ciphertexts attacks.
Gilles Barthe, Sabrina Tarento
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where TYPES
Authors Gilles Barthe, Sabrina Tarento
Comments (0)
books