Prochaine session deeptech Machine Learning and Cybersecurity: Why and How with scikit-learn avancé – le 30 octobre
Prochaine session deeptech CORESE, la boîte à outils des graphes de connaissance débutant – le 8 novembre
Prochaine session état de l’art La cybersécurité des systèmes de contrôle industriel le 12 novembre
Prochaine session deeptech RIOT, le système d’exploitation adapté à l’internet des objets débutant les 13 et 14 novembre
Prochaine session deeptech Coq, la preuve par le logiciel débutant – le 19 novembre
Les protocoles cryptographiques sont des programmes distribués dont le but est de sécuriser nos communications : garantir la sécurité de nos données mais aussi garantir l'authentification correcte ou encore la protection de la vie privée. Des exemples déployés de tels protocoles sont TLS (sous-jacent à HTTPS), 5G-AKA (dans la téléphonie mobile) ou encore le standard EMV (Europay, Mastercard, Visa) pour les paiements par cartes bancaires. Ces protocoles sont cependant d'une grande complexité et des vulnérabilités sont régulièrement découvertes. C'est pour cela que des preuves formelles garantissant leur sécurité sont devenues indispensables. © Inria / Photo B. Fourrier
Session:
Aucune session disponible actuellement.
Les méthodes formelles permettent de modéliser mathématiquement une spécification et de prouver à l’aide d’outils de vérification (e.g. ProVerif ou Tamarin) que des propriétés, également spécifiées mathématiquement, sont satisfaites. Cette pratique est aujourd’hui largement répandue: ce type d’analyse formelle a accompagné la standardisation de protocoles tels que TLS 1.3 ou 5G-AKA et a aussi permis de découvrir des failles importantes dans des protocoles déployés tels que le protocole EMV.
Cette formation orientée méthodes formelles pour les protocoles sûrs vise à donner aux ingénieurs et développeurs une base solide pour la conception des protocoles cryptographiques fiables et robustes. Pour développer de tels protocoles il est nécessaire d’apprendre à définir les scénarios et modèles de menaces ainsi que d’utiliser des outils de vérification symbolique.
Le module permet aux ingénieurs et développeurs d’acquérir les compétences suivantes :
Bases en cryptographie
Introduction
Modélisation formelle
Analyse formelle de sécurité avec ProVerif
Étude de cas
Aperçu rapide de Tamarin
Directeur de recherche
Steve Kremer est directeur de recherche au centre Inria de l’Université de Lorraine et responsable de l’équipe–projet Pesto. Il a obtenu sa thèse en 2003 à l’Université Libre de Bruxelles et son habilitation à diriger les recherches en 2010 à l’ENS Cachan. Il est spécialiste des méthodes formelles et leur application à la sécurité, en particulier aux protocoles cryptographiques. Il a obtenu une bourse ERC pour ses travaux sur la vérification de propriétés de protection de la vie privée.
© Inria / Photo G. Scagnelli
Chargé de recherche
Lucca Hirschi est chargé de recherche en cybersécurité à Inria, membre de l’équipe-projet Pesto à Nancy. Après un doctorat à l’ENS de Paris-Saclay en 2017, il a été chercheur post-doctoral à l’ETH Zürich (Suisse) pendant deux ans avant de rejoindre Inria. Il est spécialiste des méthodes formelles et leur application à la sécurité des protocoles cryptographiques.
©coll.part.
Maître de conférences
Jannik Dreier est maître de conférences à TELECOM Nancy. Il a obtenu sa thèse en 2013 à l’Université de Grenoble sur la vérification formelle des protocoles de vote et d’enchères électroniques. Expert reconnu dans les domaines de sécurité des protocoles, vérification formelle et calculs préservant la confidentialité, Jannick est un des développeurs principaux de l’outil de vérification open source Tamarin prover.
Il co-préside par ailleurs le Working Group on Formal Methods for Security.
©coll.part.
Chargé de recherche
Alexandre Debant est chargé de recherche au centre Inria de l’Université de Lorraine, et membre de l’équipe-projet Pesto. Il a obtenu sa thèse en 2020 à l’Université de Rennes 1. Ses recherches portent sur l’étude des protocoles de sécurité en utilisant des outils de preuve automatique. Il s’est notamment intéressé à la sécurité des protocoles de paiement et protocoles de vote électronique.
©coll.part.