My research interests mainly focus on formal methods for security and privacy. I design new verification techniques, algorithms and tools to effectively and efficiently analyze formal security properties. I generally enjoy research projects that combine both foundational contributions and practical applications, including analyzing real-world cryptographic protocols.
Download my CV (PDF)
[February 2019] Our paper revealing a new privacy vulnerability on all mobile communication networks (including 5G) got accepted at PoPETS’19 and got some media coverage: ZDnet 1 and 2, The Register 1 and 2, Forbes, NextInpact, EFF, International Business Times, Silicon.de.
[July 2018] Our paper presenting our comprehensive, formal analysis of authentication protocols in 5G mobile networks (as specified by 3GPP) has been accepted at CCS’18 and has led to (still ongoing) discussions with the standardization bodies (see CVD-2018-0012 on GSMA Hall of Fame). The paper attracted some media coverage: Daily Mail, The National, ACM TechNews, The Hill, SRF 4, Tages-Anzeiger (frontpage), ETHZ news (frontpage), The Courier, 20 Minuten.
I serve in the program committee of the Computer Security track at the 29th ACM Symposium on Applied Computing (SEC@SAC), 2019.
I have reviewed papers for CCS, CSF, Euro S&P, ESORICS, POST (ETAPS), the Journal of Computer Security (JCS) and the journal LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNOC).
I have participated to the following projects: joint project between Huawei Technologies Singapore Research Center and ETH Zürich on 5G protocols, ERC Starting Grant POPSTAR, ANR project Sequoia, ANR project ProSe, ANR JCJC project VIP.
Porridge is a standalone OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols. It is not restricted to the limited class of action-deterministic protocols as in prior works. It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups. Theory and practical results are described in our ESORICS’18 paper.
UKano is a tool that enables the automatic formal verification of unlinkability and anonymity for a large class of 2-agents protocols that was previously out of scope. It has been notably used to discover new attacks on ePassport protocols. I have written this tool by leveraging our new verification method proposed in our S&P’16 paper.
I have developed and implemented Partial Order Reduction techniques for a class of security protocols (those that are action-deterministic) in the tool Apte, dramatically improving its practical impact. I also have implemented a preliminary version of those techniques in the tool SPEC (more details).
More details can be found on my old website at ENS Cachan.
A comprehensive list of my talks (from <2017) can be found on my website at ENS Cachan.