Seminar details

Room 206 (2nd floor, badged access)
9 December 2021 - 14h00
Formal security proofs in a post-quantum world
by Charlie JACOMME from CISPA

Abstract: In the recent years, formals methods for security and their associated tools have been used successfully both to find novel and complex attacks on many protocols and to help in their standardization process. They however face a new challenge with the increasing probability of
quantum computers coming into the real-world: we need to be able to provide guarantees against quantum attackers.

In this talk, we will first present a broad overview of formal methods, outlining what is the general goal of the field and how we have strived toward it. We will then focus on the post-quantum issue by presenting the corresponding concrete challenges, and thus multiple ways current computational proofs of security (proof for any Polynomial Time Turing Machine attacker) can fail against a quantum attacker. We will then present the first-order logic over which Squirrel is built, the BC logic, and show based on the first part where it fails at post-quantum soundness. In a third part, we will finally present our contribution: how we made the logic and thus the Squirrel prover post-quantum sound. We will conclude by discussing some more general challenges the field may be facing in the coming years.

Contact | Site Map | Site powered by SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1818069