Computational Soundness of Formal Encryption in Coq

R.J. Corin

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

    19 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.