My PhD defense

Practical information

Date and time

Monday, 26th November 2018, 14:00.

Location

Amphi Chemla
École Normale Supérieure Paris-Saclay
61 avenue du Président Wilson
94230 Cachan

How to come

Have a look at this page for directions to the campus and then at this map to find your way around the campus. The amphi Chemla is inside the Institut D'Alembert, tagged as IDA on this map. Please note that it is not inside the D'Alembert building.

Thesis

Title

Verification of indistinguishability properties in cryptographic protocols -- Small attacks and efficient decision with SAT-Equiv.

Keywords

Cryptographic protocols, Formal methods, Symbolic model

Abstract

This thesis presents methods to verify cryptographic protocols in the symbolic model: formal methods allow to verify that small distributed programs satisfy equivalence properties. Those properties state that an attacker cannot decide what scenario is beeing played. Strong secrecy, and privacy type properties, like anonymity and unlinkeability, can be modelled through this formalism. Moreover, protocols are executed simultaneously by an unbounded number of agents, for an unbounded number of sessions, which leads to indecidability results. So, we have either to consider an arbitrary number of sessions, and search for semi-decision procedures and decidable classes; or to establish decision procedures for a finite number of sessions.

When we started the work presented in this thesis, the existing equivalence checkers in the bounded model were highly limited. They could only handle a~very small number of sessions (sometimes no more than three). This thesis presents efficient decision procedures for bounded verification of equivalence properties. Our first step is to provide small attack results. First, for deterministic processes, there exists an attack if, and ony if, there is a well-typed attack, assuming that there is no confusion between variable types. Second, when there exists a flaw, the attacker needs at most three constants to find it. Then, our second step is to translate the indistinguishability problem as a reachability problem in a planning system. We solve this second problem through planning graph algorithm and SAT encoding. In a final step, we present the implementation of the SAT-Equiv tool, which allows us to evaluate our approach. In particular, a benchmark with comparable tools proves the efficiency of SAT-Equiv.

Manuscript

It can be found here.

Jury

CHEVALIER Yannick Rapporteur
VIGANÒ Luca Rapporteur
DELAUNE Stéphanie PhD supervisor
CORTIER Véronique PhD supervisor
PALAMIDESSI Catuscia Examinator
COMPAGNA Luca Examinator
LUBICZ David Examinator

About LSV