UK-SPS Seminar: 18th May - Title: The security protocol verifier ProVerif....

The UK-SPS Seminar this week will be as follows: 

Time: Wed, May 18, 15:00 – 16:00 (UK Time) 

Attendance via Zoom (ID: 834 8186 6474, Passcode: 032120)

Livestream via Youtube

Speaker: Bruno Blanchet (INRIA)

Joint talk with the FM-SEC network

Title: The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more

Abstract: ProVerif is a widely used automatic security protocol verifier that relies on symbolic model of cryptography. It can prove various security properties (secrecy, correspondences, some equivalences) for an unbounded number of sessions, as well as find attacks. In this talk, we will present an overview of ProVerif and its recent improvements. These improvements are twofold. First, we extended ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we reworked and optimized many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, …), resulting in impressive speed-ups on large examples. These improvements are joint work with Vincent Cheval and Véronique Cortier, to appear at IEEE Security and Privacy 2022.

Bio: Bruno Blanchet is a senior researcher at Inria, in Paris, France, in the Prosecco research team. From 2001 to 2010, he was a researcher at CNRS, in École Normale Supérieure, Paris, France and from 2001 to 2004, he was an independent research group leader at Max Planck Institute for Computer Science, Saarbrücken, Germany. He also worked for Polyspace Technologies, Bell Labs Research, Google, and Nomadic Labs on short-term contracts. After a PhD on program analysis by abstract interpretation, he specialized on the verification of security protocols. He is the main designer and implementer of two protocol verification tools: ProVerif, which relies on the symbolic model of cryptography, and CryptoVerif, which produces security proofs in the computational model of cryptography, like those manually written by cryptographers. He published more than 50 research papers in major conferences (IEEE S&P, CCS, CSF, CRYPTO, EuroCrypt, POPL, ...) and journals (JACM, TISSEC, JCS, ...).

Please feel free to forward to others who might be interested. 

UK-SPS is an inter-university seminar series on cyber security and privacy. Seminar details are also advertised on our website, calendar and Twitter, and recordings will be available on our YouTube channel afterwards. 

Last modified: Mon, 16 May 2022 12:19:32 BST