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

    23 Citations (Scopus)
    93 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
    Event2nd International Joint Conference on Automated Reasoning, IJCAR 2004 - Cork, Ireland
    Duration: 4 Jul 20048 Jul 2004

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer-Verlag
    Volume3097

    Conference

    Conference2nd International Joint Conference on Automated Reasoning, IJCAR 2004
    Period4/07/048/07/04
    OtherJuly 4-8, 2004

    Keywords

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

    Cite this