Formal security proofs in a post-quantum world

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 [A] 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.[A] see, e.g., https://www.bbc.co.uk/news/technology-58719891 for a recent example[B] https://squirrel-prover.github.io/