Crypto-Verifying Protocol Implementations in ML

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

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

    31 Downloads (Pure)


    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 languageEnglish
    Title of host publication3rd Workshop on Formal and Computational Cryptography, FCC 2007
    Place of PublicationFrance
    Number of pages6
    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


    Workshop3rd Workshop on Formal and Computational Cryptography, FCC 2007
    Abbreviated titleFCC


    • SCS-Cybersecurity


    Dive into the research topics of 'Crypto-Verifying Protocol Implementations in ML'. Together they form a unique fingerprint.

    Cite this