A Machine-Checked Formalization of the Generic Model and the Random Oracle Model

Gilles Barthe, J.G. Cederquist, Sabrina Tarento

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    20 Citations (Scopus)
    39 Downloads (Pure)

    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.
    Original languageUndefined
    Title of host publication2nd International Joint Conference on Automated Reasoning, IJCAR
    EditorsDavid Basin, Michaël Rusinowitch
    Place of PublicationBerlin
    PublisherSpringer
    Pages385-399
    Number of pages15
    ISBN (Print)3-540-22345-2
    DOIs
    Publication statusPublished - Jul 2004

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer-Verlag
    Volume3097

    Keywords

    • METIS-220259
    • IR-48633
    • SCS-Cybersecurity
    • EWI-755

    Cite this

    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