VeriCrypt: An Introduction to Tools for Verified Cryptography

10th-11th December, 2020

Aims and Objectives

Recent years have witnessed a spurt in the design and deployment of novel and complex cryptographic constructions and protocols, motivating the need for formal methods and verification tools that can verify the security of these mechanisms and the correctness of their implementations. A variety of tools have been proposed to address this need. The goal of this tutorial is to give attendees an introduction to the following four formal verification tools that can be applied to obtain higher confidence in cryptographic constructions, protocols, and implementations:


The main pre-requisites are a willingness to learn and comfort with programming, cryptography, and formal logic. Each tutorial will include an introductory lecture and a hands-on demo. Attendees will be given a set of exercises they can do on their own after the workshop and submit to the speakers. We will also make available an online chat forum where students can ask questions and interact with the speakers.

For a full survey of relevant tools and case studies in this domain, and a discussion of their limitations and comparative strengths, see this systematization-of-knowledge paper.


  • Dates: 10th-11th December, 2020
  • Registration Deadline: 30th November, 2020


Tamarin Prover
December 10, 13:00 - 15:30 IST

Speaker: Cas Cremers

Tamarin is a verification tool that relies on a symbolic (or Dolev-Yao) model of cryptography. It has been used to verify and find flaws in a wide variety of protocols, including TLS 1.3 and 5G-AKA.

December 10, 16:00 - 18:30 IST

Speaker: Bruno Blanchet, Benjamin Lipp

CryptoVerif is a prover that relies on a computational (or complexity-theoretic) model of cryptography. It has been used to develop machine-checked proofs of protocols like TLS 1.3 and WireGuard.

December 11, 13:00 - 15:30 IST

Speakers: Aseem Rastogi, Marina Polubelova

F* is a general-purpose programming language and security-oriented verification framework. It has been used to develop verified high-performance implementations of cryptographic algorithms in the HACL* library as well as verified implementations of protocols like Signal and TLS 1.3.

December 11, 16:00 - 18:30 IST

Speakers: Pierre-Yves Strub, Manuel Barbosa

EasyCrypt is a toolset for construction and verification of game-based cryptographic proofs. It has been used to develop proofs of the proofs of the AWS Key Management service as well as a verification backend for verified assemly implementations of cryptographic primitives written in the Jasmin language.

Organised By

Karthikeyan Bhargavan
Aseem Rastogi
Microsoft Research

With Support From