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.