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 ProverDecember 10, 13:00 - 15:30 IST
Speaker: Cas Cremers
CryptoverifDecember 10, 16:00 - 18:30 IST
F*December 11, 13:00 - 15:30 IST
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.
EasyCryptDecember 11, 16:00 - 18:30 IST
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.