@inproceedings{a7b7ee67682d4d85b1a05dcacf37caa2,
title = "A Machine-Checked Formalization of the Generic Model and the Random Oracle Model",
abstract = "Most approaches to the formal analyses of cryptographic protocols make the perfect cryptography assumption, i.e. the hypothese that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. Ideally, one would prefer to rely on a weaker hypothesis on the computational cost of gaining information about the plaintext pertaining to a ciphertext without knowing the key. Such a view is permitted by the Generic Model and the Random Oracle Model which provide non-standard computational models in which one may reason about the computational cost of breaking a cryptographic scheme. Using the proof assistant Coq, we provide a machine-checked account of the Generic Model and the Random Oracle Model.",
keywords = "METIS-220259, IR-48633, SCS-Cybersecurity, EWI-755",
author = "Gilles Barthe and J.G. Cederquist and Sabrina Tarento",
note = "Imported from DIES; 2nd International Joint Conference on Automated Reasoning, IJCAR 2004 ; Conference date: 04-07-2004 Through 08-07-2004",
year = "2004",
month = jul,
doi = "10.1007/978-3-540-25984-8_29",
language = "Undefined",
isbn = "3-540-22345-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "385--399",
editor = "David Basin and Micha{\"e}l Rusinowitch",
booktitle = "2nd International Joint Conference on Automated Reasoning, IJCAR",
address = "Germany",
}