ANR Project
TECAP

TECAP: Protocol Analysis - Combining Existing Tools

ANR-17-CE39-0004-01

Meeting 08/07/2019

The meeting of the ANR Project TECAP was held on July 08 2019 at LIX.

Venue

The meeting will be held in the Philippe Flajolet room in the Alan Turing building of the polytechnique campus.

Program

10:00 Welcome coffee

10:20 Vincent Cheval: Short welcome

10:30 Benjamin Lipp: A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.

11:10 Pierre-Yves Strub: Report on linking CryptoVerif & EasyCrypt : dealing with concrete complexity in EasyCrypt

11:50 Lunch

13:20 Vincent Cheval: Efficient verification of trace equivalences in finite process-calculi

In this paper we improve the efficiency of automated verification of privacy type properties in cryptographic protocols. Formalised as an observational equivalence in concurrent process calculi, the underlying problem is undecidable in general and, for some classes of common cryptographic primitives, coNEXP-complete when the number of honest protocol sessions is bounded. We develop optimisation techniques for verifying such equivalences, exploiting the symmetries between and within the two processes under study. We integrated our work in the recent automated verification tool, DeepSec, demonstrating a significant speed-up during practical verification, thus increasing the size and scope of the protocols that can be analysed fully automatically in practice.

14:00 Ivan Gazeau: Akiss reloaded: harder, better, faster, stronger

In this talk, I will present a new algorithm for Akiss, a tool which decide equivalence of cryptographic protocols in the symbolic model. This upgraded tool is able to decide the exact trace equivalence property in an efficient way due to a better handling of concurrency.

14:40 Solène Moreau : Unlinkability for stateful protocols

15:20 Coffee Break

15:50 Vincent Cheval: An overview of the new upcoming features in ProVerif

16:30 Jannik Drier: Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR