Computational Soundness of Formal Encryption in Coq

R.J. Corin

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

    15 Downloads (Pure)

    Abstract

    We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.
    Original languageUndefined
    Title of host publication3rd Workshop on Formal and Computational Cryptography, FCC 2007
    Place of PublicationFrance
    PublisherINRIA
    Pages-
    Number of pages6
    ISBN (Print)not assigned
    Publication statusPublished - 4 Jul 2007
    Event3rd Workshop on Formal and Computational Cryptography, FCC 2007 - Venice, Italy
    Duration: 4 Jul 20075 Jul 2007
    Conference number: 3

    Publication series

    Name
    PublisherINRIA
    Number06472

    Workshop

    Workshop3rd Workshop on Formal and Computational Cryptography, FCC 2007
    Abbreviated titleFCC
    CountryItaly
    CityVenice
    Period4/07/075/07/07

    Keywords

    • EWI-10233
    • IR-64106
    • METIS-241659
    • SCS-Cybersecurity

    Cite this

    Corin, R. J. (2007). Computational Soundness of Formal Encryption in Coq. In 3rd Workshop on Formal and Computational Cryptography, FCC 2007 (pp. -). France: INRIA.
    Corin, R.J. / Computational Soundness of Formal Encryption in Coq. 3rd Workshop on Formal and Computational Cryptography, FCC 2007. France : INRIA, 2007. pp. -
    @inproceedings{683955a4cefb439596606a1f840c6379,
    title = "Computational Soundness of Formal Encryption in Coq",
    abstract = "We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.",
    keywords = "EWI-10233, IR-64106, METIS-241659, SCS-Cybersecurity",
    author = "R.J. Corin",
    year = "2007",
    month = "7",
    day = "4",
    language = "Undefined",
    isbn = "not assigned",
    publisher = "INRIA",
    number = "06472",
    pages = "--",
    booktitle = "3rd Workshop on Formal and Computational Cryptography, FCC 2007",

    }

    Corin, RJ 2007, Computational Soundness of Formal Encryption in Coq. in 3rd Workshop on Formal and Computational Cryptography, FCC 2007. INRIA, France, pp. -, 3rd Workshop on Formal and Computational Cryptography, FCC 2007, Venice, Italy, 4/07/07.

    Computational Soundness of Formal Encryption in Coq. / Corin, R.J.

    3rd Workshop on Formal and Computational Cryptography, FCC 2007. France : INRIA, 2007. p. -.

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

    TY - GEN

    T1 - Computational Soundness of Formal Encryption in Coq

    AU - Corin, R.J.

    PY - 2007/7/4

    Y1 - 2007/7/4

    N2 - We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.

    AB - We formalize Abadi and Rogaway's computational soundness result in the Coq interactive theorem prover. This requires to model notions of provable cryptography like indistinguishability between ensembles of probability distributions, PPT reductions, and security notions for encryption schemes. Our formalization is the first computational soundness result to be mechanized, and it shows the feasibility of rigorous reasoning of computational cryptography inside a generic interactive theorem prover.

    KW - EWI-10233

    KW - IR-64106

    KW - METIS-241659

    KW - SCS-Cybersecurity

    M3 - Conference contribution

    SN - not assigned

    SP - -

    BT - 3rd Workshop on Formal and Computational Cryptography, FCC 2007

    PB - INRIA

    CY - France

    ER -

    Corin RJ. Computational Soundness of Formal Encryption in Coq. In 3rd Workshop on Formal and Computational Cryptography, FCC 2007. France: INRIA. 2007. p. -