Research Themes

Cryptographic protocols

Real-World Protocols Analysis: In practice, cryptographic protocols are difficult to design and to properly implement. We aim at analysing the security of such protocols in the context of international standards (e.g. W3C) and industrial specifications (e.g. GlobalPlatform). In particular, we examine all forms in which a protocol comes: abstraction design, wordy description, and software implementation. Recently, our work was recognized by Google, ProtonMail, GlobalPlatform and the GSM Association.
Protocol Design: We are interested in protocols for low-resource devices. We aim at designing protocols that provide better security guarantees for constrained devices. In addition, we look at distance-bounding protocols not only on contactless devices, but also on the Internet.
Software Vulnerabilities: Our experience shows that the mathematical abstraction of cryptographic protocols does not always capture what can happen in practice. Many protocols proven secure have been attacked because of vulnerabilities in their implementations. We are particularly interested in cryptographic attacks (e.g. padding oracle), constant-time execution, micro-architectural leaks, formally-proved implementations, and software-based protections (e.g. whitebox). Our patches exist in various projects: OpenSSL, FreeRadius, etc.

Attacking privacy-preserving data publishing schemes: We aim at stress-testing privacy-preserving data publishing schemes by designing attacks based on machine learning techniques and inspired from real-life publishing use-cases and attackers. We are especially interested in differentially private publishing schemes and in time series data.
Privacy-preserving data-intensive algorithms: We aim at developing the joint use of differentially private perturbation schemes with encryption schemes for contributing to the design of efficient privacy-preserving database management systems and privacy-preserving analytical systems. Our goal is threefold: rationalize the use of perturbation techniques for computation, rethink the classical system architectures, and study the combination of specific encryption schemes with perturbation schemes.
E-voting & Unlinkability: We are interested in vote privacy properties for electronic voting protocols. Our work aims in particular at formally defining vote privacy in a context where election authorities are untrusted. We also study how vote privacy, as well as other privacy related properties (e.g. unlinkability, anonymity) can be efficiently verified in the symbolic model using automated tools. Two papers on unlinkability and vote privacy have received a distinguished paper award at the Computer Security Foundations Symposium (CSF) in 2020.

Verification of protocols: We aim at developing rigorous techniques to ensure that the security protocols we are using are safe. In particular, we are currenly developing the Squirrel Prover, an interactive prover for protocols. While reasoning inside a first-order logic, it allows to obtain computational guarantees. This research theme is at the heart of the ERC project POSPTAR and the ANR project TECAP.
Graphical models for security: We are working on enhancing risk assessment processes with graph-based approaches, such as attack trees and attack-defense trees.
We mainly focus on methods for efficient quantitative analysis of security and algorithms for identifying optimal attacks and countermeasures. We are also interested in automated generation of attack tree-like models.