CryptoVerif tutorial

This tutotial was given at the VeriCrypt event associated to Indocrypt 2020.

Note: This tutorial uses the so-called "oracle" front-end of CryptoVerif, a syntax designed to be closer to the syntax of games used by cryptographers in manual proofs.

  1. First part: encrypt-then-MAC example
  2. Second part: signed Diffie-Hellman example
  3. Exercises

Bruno Blanchet Benjamin Lipp