Crypto-Verifying Protocol Implementations in ML

K. Bhargavan, R.J. Corin, C. Fournet

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

    21 Downloads (Pure)

    Abstract

    We intend to narrow the gap between concrete implementations and verified models of cryptographic protocols. We consider protocols implemented in F#, a variant of ML, and verified using CryptoVerif, Blanchet's protocol verifier for computational cryptography. We experiment with compilers from F# code to CryptoVerif processes, and from CryptoVerif declarations to F# code. We present two case studies: an implementation of the Otway-Rees protocol, and an implementation of a simplified password-based authentication protocol. In both cases, we obtain concrete security guarantees for a computational model closely related to executable code.
    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-10234
    • IR-64107
    • METIS-241660
    • SCS-Cybersecurity

    Cite this

    Bhargavan, K., Corin, R. J., & Fournet, C. (2007). Crypto-Verifying Protocol Implementations in ML. In 3rd Workshop on Formal and Computational Cryptography, FCC 2007 (pp. -). France: INRIA.