Vincent Cheval Chargé de Recherche Inria Paris
Vincent Cheval's Photoghaph

Recent activities

Updated the 22/02/2023 (This news section is not regularly updated though I try to keep my publication page up to date.

Since 12/2022: Currently visiting University of Oxford. Currently working on the next release of ProVerif 2.05

2022 was a good year in term of publications: One publication at S&P on ProVerif, one at CCS on verification of TLS with the Encrypted Client Hello extension, one at USENIX on the platform SAPIC+ and finally one publication at CSF on probabilistic applied pi calculus and equivalence properties.

Following the shutdown of Gforge server, I had to change my webpage. It was unaccessible for a while but it's back !

10/09/2021: Bruno Blanchet and I are happy to announce a new release of ProVerif, version 2.03, available at

03/07/2021: Our paper ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. has been accepted for publication in IEEE Security and Privacy 2022.

01/01/2021: Our paper The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. has been accepted for publication in Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday.

01/09/2020: I've moved from Inria Grand Est to Inria Paris within the PROSECCO team.

22/01/2020: Our paper On the semantics of communications when verifying equivalence properties has been accepted for publication in the Journal of Computer Security.

18/01/2020: The new version of DeepSec will soon be released. We're currently during the alpha stage but we hope that the official realease will come shortly. This release will also be shipped with the release of a brand new user interface DeepSec UI. Amongst the new features:

  • Improved efficiency when verifying queries.
  • Support for "Eavesdrop", "Classic" and "Private" semantics (POST'17) for verifying trace equivalence.
  • Integration and improvements of session equivalence (CCS'19).
  • Recording of the result of your runs that can be displayed in DeepSec UI.
  • DeepSec UI supports all of DeepSec's abilities does but with a nice interface.
  • Interactive display of attacks for violated queries.
  • Interactive simulator for equivalence for verified queries.

11/11/2019: Our paper Exploiting Symmetries When Proving Equivalence Properties for Security Protocols was presented at the 26th ACM Conference on Computer and Communications Security, held in London

22/05/2018: We received a Distinguished Paper Award at the 2018 IEEE Symposium on Security and Privacy for our paper DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice.. See the Twitter post.