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)
[Summer 2019] The privacy attack on 5G (and also on 3G and 4G) we disclosed in our PETS’19 paper has been added to the list of key issues in 5G authentication (see Technical Report 33.846). Various vendors have proposed to 3GPP several change requests (CRs) with dedicated countermeasures (see the CR from Qualcomm, Gemalto, ChinaMobile, Thales, Nokia, ZTE, and Huawei).
[February 2019] Our paper revealing a new privacy vulnerability on all mobile communication networks (including 5G) got accepted at PETS’19 and got some media coverage: ZDnet 1 and 2, The Register 1 and 2, Forbes, NextInpact, EFF, International Business Times, Silicon.de.
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.