VeriCrypt: An Introduction to Tools for Verified Cryptography

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:

Prerequisites

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.

Register

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

Schedule