PhD Defence

Adrien Koutsos

Manuscript and Slides

The manuscript is available here.
The slides of the defence.

General Information

I defended my thesis, entitled "Symbolic Proofs of Computational Indistinguishability", on Friday 27th of September, 2019, at 14:00 in the conference room of the Pavillon des Jardins, at the ENS Paris-Saclay.

Jury

Catuscia Palamidessi (INRIA, Ecole Polytechnique), president
Cas Cremers (Cispa Helmholtz), reviewer
Bogdan Warinschi (Bristol University), reviewer
Myrto Arapinis (Edinburgh University), examiner
Bruno Blanchet (INRIA Paris), examiner
Hubert Comon (ENS Paris-Saclay), advisor

Abstract

Our society extensively relies on communications systems. Because such systems are used to exchange sensitive information and are pervasive, they need to be secured. Cryptographic protocols are what allow us to have secure communications. It is crucial that such protocols do not fail in providing the security properties they claim, as failures have dire consequences. Unfortunately, designing cryptographic protocols is notoriously hard, and major protocols are regularly and successfully attacked. We argue that formal verification is the best way to get a strong confidence in a protocol security. Basically, the goal is to mathematically prove that a protocol satisfies some security property.

Our objective is to develop techniques to formally verify equivalence properties of cryptographic protocols, using a method that provides strong security guarantees while being amenable to automated deduction techniques. In this thesis, we argue that the Bana-Comon model for equivalence properties meets these goals. We support our claim through three different contributions.

First, we design axioms for the usual functions used in security protocols, and for several cryptographic hypothesis. Second, we illustrate the usefulness of these axioms and of the model by completing case studies of concrete protocols: we study two RFID protocols, KCL and LAK, as well as the 5G-AKA authentication protocol used in mobile communication systems. For each of these protocols, we show existing or new attacks against current versions, propose fixes, and prove that the fixed versions are secure. Finally, we study the problem of proof automation in the Bana-Comon model, by showing the decidability of a set of inference rules which is a sound, though incomplete, axiomatization of computational indistinguishability when using an IND-CCA2 encryption scheme. From a cryptographer's point of view, this can be seen as the decidability of a fixed set of cryptographic game transformations.