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