Introduction Using CryptoVerif Proof technique Enc then MAC example FDH example Conclusion

Introduction Using CryptoVerif Proof technique Enc-then-MAC example FDH example Conclusion CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA, Paris September 2009 Bruno Blanchet (CNRS, ENS, INRIA) CryptoVerif September 2009 1 / 72

• cryptographic primitives


• cryptoverif proof technique


• proofs can


• bitstrings cryptographic primitives


• approach allows


• direct approach


• dolev-yao model


• automatic proof