Séminaire

Date : 25 novembre 2021 15:20 - Salle :Grand amphi SIGMA Formal security proofs in a post-quantum world Charlie JACOMME - Post-doc au CISPA (Allemagne)

Le séminaire sera dans l'Amphi Blaise Pascal aussi simplement appelé "grand amphi"

Pour venir :

Accès depuis le grand hall d'entrée - le grand hall se situe tout en bas de la géode, directement après l'entrée principale (tout en bas de Sigma).

En entrant par le haut de Sigma, l'entrée par laquelle on arrive depuis l'ISIMA, il faut aller dans la géode et descendre l'escalier jusqu'à arriver

au grand hall.

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.

https://charlie.jacomme.fr/fr/

[A] see, e.g., https://www.bbc.co.uk/news/technology-58719891 for a recent example

[B] https://squirrel-prover.github.io/