VeriCrypt: An Introduction to Tools for Verified Cryptography

18th-19th December, 2021

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 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: 18th-19th December, 2021
  • Registration Deadline: 10th December, 2021
  • FSTTCS and VeriCrypt Basic Registration: Register here

Materials and Communication

Schedule

Introduction: Formal Verification meets Applied Cryptography
December 18, 12:00 - 12:30 IST

Speaker: Karthikeyan Bhargavan

ProVerif
December 18, 12:30 - 17:15 IST

Speakers: Bruno Blanchet and Vincent Cheval

ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signatures), hash functions, and Diffie-Hellman key agreements, specified both as rewrite rules or as equations. It can handle an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space.

ProVerif has been used to develop machine-checked symbolic security proofs for a variety of real-world protocols, including TLS 1.3. See this paper for a detailed survey of research on ProVerif.

Sessions:
Time Session Speaker
12:30 - 13:30 Introduction to Symbolic and Computational Proofs Bruno Blanchet
13:45 - 15:15 ProVerif Tutorial Vincent Cheval
15:30 - 16:30 Advanced topics in symbolic analysis Vincent Cheval
16:45 - 18:15 Advanced ProVerif Tutorial Vincent Cheval
F*
December 19, 10:00 - 15:30 IST

Speakers: Aseem Rastogi and Abhishek Bichhawat

F* is a general-purpose, proof-oriented programming language. It has been used to prove correctness and security of critical code in several domains. For example, low-level parsers proven in F* are currently deployed in Windows Hyper-V. F* has also 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. Some of these cryprogrpahic primitives have been deployed in the Firefox browser and the Linux kernel.

We will start with a broad overview of F*, its applications, and ongoing research. We will then get into the internals of F* and learn about its main features with the help of several examples. In this part, we will also cover recent work on embedding and programming with a higher-order concurrent separation logic in F*. Finally, we will have a couple of sessions on F* applications--we will learn about the EverParse library for automatically generating low-level formally proven parsers and DY*, a framework for symbolic analysis of crypographic protocols.

Sessions:
Time Session Speaker
10:00 - 11:00 Overview of F*, applications, and deployments Aseem Rastogi
11:15 - 13:00 F* tutorial (main features, examples, recent work on separation logic in F*) Aseem Rastogi
13:15 - 14:00 EverParse/3D : A tool for automatically generating verified low-level parsers Tahina Ramananandro‬ and Aseem Rastogi
14:15 - 15:30 DY* : Symbolic Verification of Cryptographic Protocols Abhishek Bichhawat

Previous Editions


Organisers

Karthikeyan Bhargavan
INRIA Paris
France
Aseem Rastogi
Microsoft Research
India