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.
- First part: encrypt-then-MAC example
- Second part: signed Diffie-Hellman example
- Recorded video