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.
|Title of host publication||2nd International Joint Conference on Automated Reasoning, IJCAR|
|Editors||David Basin, Michaël Rusinowitch|
|Place of Publication||Berlin|
|Number of pages||15|
|Publication status||Published - Jul 2004|
|Name||Lecture Notes in Computer Science|
Barthe, G., Cederquist, J. G., & Tarento, S. (2004). A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin, & M. Rusinowitch (Eds.), 2nd International Joint Conference on Automated Reasoning, IJCAR (pp. 385-399). (Lecture Notes in Computer Science; Vol. 3097). Berlin: Springer. https://doi.org/10.1007/978-3-540-25984-8_29