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:
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: 18th-19th December, 2021
- Registration Deadline: 10th December, 2021
- FSTTCS and VeriCrypt Basic Registration: Register here
Materials and Communication
Introduction: Formal Verification meets Applied CryptographyDecember 18, 12:00 - 12:30 IST
Speaker: Karthikeyan Bhargavan
ProVerifDecember 18, 12:30 - 17:15 IST
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.
|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
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.
|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|