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 language | English |
---|---|
Title of host publication | 3rd Workshop on Formal and Computational Cryptography, FCC 2007 |
Place of Publication | France |
Publisher | INRIA |
Number of pages | 6 |
Publication status | Published - 4 Jul 2007 |
Event | 3rd Workshop on Formal and Computational Cryptography, FCC 2007 - Venice, Italy Duration: 4 Jul 2007 → 5 Jul 2007 Conference number: 3 |
Workshop
Workshop | 3rd Workshop on Formal and Computational Cryptography, FCC 2007 |
---|---|
Abbreviated title | FCC |
Country/Territory | Italy |
City | Venice |
Period | 4/07/07 → 5/07/07 |
Keywords
- SCS-Cybersecurity