- This seminar has passed.
[Joint FM-SEC talk] The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more
18 May 2022 @ 3:00 pm - 4:00 pm
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.
Joint talk with the FM-SEC network.
Zoom meeting: https://newcastleuniversity.zoom.us/j/83481866474?pwd=Qjl4NDZvQ0l1V1ByU1l3SUg3eTZIUT09
Meeting ID: 834 8186 6474
Passcode: 032120
Youtube live streaming: https://youtu.be/IYOl3AKXdkA
Presenter
-
Bruno Blanchet (INRIA)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, ...).