Vincent Cheval
Vincent Cheval
Department of Computer Science,
Robert Hooke Building,
Room 116
Directions Postal Address
Interests
My research area is the formal analysis and design of cryptographic protocols, with an emphasis on automated verification in the so-called symbolic model and the development of state-of-the-art verification tools. The theories behind my research and tools have root in automated reasoning, rewriting, (probabilistic) model-checking, first-order logic and concurrency theory. Originally, I mainly focused on privacy-type security properties such as anonymity, privacy, unlinkability, strong secrecy that can be expressed by the means of behavioral equivalences. Since 2018, through my work on ProVerif, I have tackled a broader set of security properties, including for example accountability, injective-correspondence, end-to-end verifiability, liveness. My research aims at verifying relevant security protocols, e.g. TLS, cryptocurrency blockchain based protocols, electronic voting protocols, RFID protocols, certificate management protocols, telecommunication protocols, cloud computing...
Biography
Vincent is an Associate Professor at the Department of Computer Science, University of Oxford. Before coming to Oxford, he was a "Chargé de Recherche" (permanent researcher) at Inria, first in Nancy (France) in the PESTO team from 2015 to 2020, and then in Paris (France) in the PROSECCO team from 2020 to 2023. He was a postdoctoral reasearcher with Prof. Mark Ryan at the University of Birmingham (UK) from 2013 to 2014, and a lecturer in University of Kent in 2015 before joining INRIA. He obtained his PhD from Ecole Normale Supérieure de Cachan (ENS-Cachan) under supervision of Prof. Hubert Comon and Prof. Stéphanie Delaune. He also obtained his MSc from ENS-Cachan.
My CV can be found here.
Graduate Students
I am actively looking for new PhD students interested in working on topics related to my research interests, and particularly on verification of cryptographic protocols. I am also open to new research topics that students would like to pursue. In general, it is good to have a strong theoretical background on logic, model checking, automated verification, formal models, etc. but I am also interested in students that are keen to implement tools.
If you are interested, you can contact me by email but you can also directly apply to the DPhil at the Computer Science Department at Oxford (see webpage). The department has some scholarship available (deadline is 01/12/2023).
Teaching
Lectures within the department:
- [Hillary2024] Concurrent Programming
I am also a tutorial fellow at Balliol College.
Tools
An important part of my research focuses on enhancing the scope, efficiency, and usability of verification tools for cryptographic protocols. Altough, recently, I am mostly working on ProVerif, I worked on the developement (theoretical and/or implementation) of the following tools:
- DeepSec: DEciding Equivalence Properties in SECurity protocols
- ProVerif: Cryptographic protocol verifier in the formal model
- SAPIC+ (included in Tamarin): Generic process plateform translating in both Tamarin and ProVerif
- Akiss: Tool for checking trace equivalence for security protocols
- Adecs: A decision algorithm for proving symbolic equivalence of constraint systems
- APTE: Algorithm for Proving Trace Equivalence
Selected Publications
-
On Learning Polynomial Recursive Programs
Alex Buna−Marginean‚ Vincent Cheval‚ Mahsa Shirmohammadi and James Worrell
In Proc. ACM Program. Lang.. Vol. 8. No. POPL. 2024.
To appear January 2024.
Details about On Learning Polynomial Recursive Programs | BibTeX data for On Learning Polynomial Recursive Programs | DOI (10.1145/3632876)
-
Symbolic protocol verification with dice
Vincent Cheval‚ Raphaëlle Crubillé and Steve Kremer
In J. Comput. Secur.. Vol. 31. No. 5. Pages 501–538. 2023.
Details about Symbolic protocol verification with dice | BibTeX data for Symbolic protocol verification with dice | DOI (10.3233/JCS-230037) | Download (pdf) of Symbolic protocol verification with dice
-
Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses
Vincent Cheval‚ Cas Cremers‚ Alexander Dax‚ Lucca Hirschi‚ Charlie Jacomme and Steve Kremer
In Joseph A. Calandrino and Carmela Troncoso, editors, 32nd USENIX Security Symposium‚ USENIX Security 2023‚ Anaheim‚ CA‚ USA‚ August 9−11‚ 2023. Pages 5899–5916. USENIX Association. 2023.
Distinguish Paper Award
Details about Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses | BibTeX data for Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses | Download (pdf) of Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses