CVK: Crypto Verification Kit
Cryptographic protocols often go wrong; even experts can and do miss bugs. Our tools analyze reference implementations of protocols, proving security theorems, or finding vulnerabilities. Successfully applied to TLS, Windows Cardspace, Web Services.
Tools in the Crypto Verification Kit
- F# is our selected language for writing security critical software.
- FS2PV, developed as part of the Samoa project on web services security, translates F# programs for analysis with Blanchet's ProVerif.
- FS2CV, developed at the MSR-INRIA Joint Centre, translates F# programs for analysis with Blanchet's CryptoVerif.
- F7 is an enhanced typechecker for F#, able to check security properties of cryptographic protocols and APIs.
Selected Publications
- Karthikeyan Bhargavan, Ricardo Corin, Cedric Fournet, and Eugen Zalinescu, Cryptographically verified implementations for TLS, in 15th ACM Conference on Computer and Communications Security (CCS'08), Association for Computing Machinery, Inc., October 2008
- Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis, Refinement Types for Secure Implementations, no. MSR-TR-2008-118, September 2008
- Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Stephen Tse, Verified Interoperable Implementations of Security Protocols, no. MSR-TR-2006-46, September 2007
