Skip to main content

Vincent Cheval

Personal photo - Vincent Cheval

Vincent Cheval

Associate Professor

Tutorial Fellow, Balliol College

T: 01865 283667

Department of Computer Science,
Robert Hooke Building, Room 116
Directions Postal Address


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...


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).


Lectures within the department:

I am also a tutorial fellow at Balliol College


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

View AllManage publications