Description
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/
Infos pratiques
Prochains exposés
-
Les jeux vidéo de l’écran au réel : enjeux juridiques et (géo)politiques au prisme de la cybersécurité
Orateur : Léandre Lebon, Sandrine Turgis - Univ Rennes, IODE
Protection des droits d’auteur, lutte contre les techniques de triche, interactions avec la guerre et les conflits hybrides, enjeux de démocratie ... Sous l’angle de la cybersécurité les enjeux juridiques et (géo)politiques des jeux video sont nombreux. Cette présentation du groupe de travail sur les jeux video (GTJV) permettra d’alimenter la réflexion sur l’articulation entre jeux video et[…]-
Law
-
-
The Quest for my Perfect MATE. Investigate MATE: Man-at-the-End attacker (followed by a hands-on application).
Orateur : Mohamed Sabt, Etienne Nedjaï - Univ Rennes, IRISA
Shannon sought security against an attacker with unlimited computational powers: if an information source conveys some information, then Shannon’s attacker will surely extract that information. Diffie and Hellman refined Shannon’s attacker model by taking into account the fact that the real attackers are computationally limited. This idea became one of the greatest new paradigms in computer[…]