An Introduction to Game-Based Cryptographic Proofs with the CryptoVerif Proof AssistantSlides I Slides II Extra
Abstract: Provable security provides the strongest assurance of cryptographic security on the specification level of a cryptosystem. However, writing and verifying proofs is a delicate task. Automated tools can help reduce errors and reviewing load.
CryptoVerif is a proof assistant for game-based cryptographic proofs used for analyses in the asymptotic and the concrete security framework. It formalizes code-based proofs by sequences of games (“game hopping”), and has a high degree of automation which allows treating complex protocols. The tool has been used to write proofs for SSH, TLS, the Signal protocol, the WireGuard VPN protocol, and during the development of the HPKE standard.
CryptoVerif only requires users to specify the initial game and the proof goals (secrecy, authentication, or indistinguishability) and will then try to carry out the proof automatically through its built-in strategy. Users can alternatively guide the proof by manually specifying some proof steps. The tool comes with a predefined set of cryptographic assumptions, and users can also specify their own using CryptoVerif’s input language.
This tutorial will teach participants to read and understand the security notions expressed in most existing CryptoVerif models. We will guide them through multiple examples, first covering some classical cryptographic assumptions (DDH, ROM, EUF-CMA) applied to constructions like Encrypt-Then-Mac, and then looking at small protocols like a signed Diffie-Hellman key exchange. The tutorial will include a gentle reintroduction to provable security and game-based/code-based/game hopping proofs. Participants should bring a laptop.