Prochaine session deeptech CORESE, la boîte à outils des graphes de connaissances débutant le 15 avril

Prochaine session deeptech SOFA, le moteur de simulation multiphysique débutant et avancé le 22 avril (course in English!)

Prochaine session deeptech Scikit-learn, la boîte à outils de l’apprentissage automatique avancé les 23 et 24 avril

Prochaine session deeptech Analyse des données de santé sensibles par l’apprentissage fédéré le 4 juin (NOUVEAU !)

Prochaine session executive education Apprentissage automatique, les briques technologiques pour les PME le 5 juin

Toutes nos formations
Méthodes formelles

Méthodes formelles pour les protocoles de sécurité

 Module deeptech 
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.

Contactez-nous !

Objectifs

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 :

  • Apprendre à modéliser un protocole cryptographique.
  • Apprendre à modéliser une propriété de sécurité (authentification, secret, …).
  • Apprendre à définir correctement les scénarios et notamment les modèles de menaces (threat model) à étudier (nombre non–borné de sessions, corruption, insider/outsider, …).
  • Apprendre à utiliser et exploiter un outil de vérification symbolique (ProVerif ou Tamarin) pour mener à bien des analyses formelles de protocoles cryptographiques.

Pré-requis

Bases en cryptographie

Programme

Jour 1 (6h)

Introduction

  • Aperçu des protocoles cryptographiques
  • Pourquoi est-il si difficile de concevoir de tels protocoles et pourquoi avons-nous besoin de méthodes formelles ?
  • Périmètre des méthodes formelles : limitations et succès
  • Aperçu des outils de vérification à l’état de l’art dans le modèle symbolique

Modélisation formelle

  • Aperçu des modèles symboliques pour les protocoles cryptographiques
  • Comment modéliser les messages et la cryptographie
  • Comment modéliser les protocoles cryptographiques
  • Comment modéliser les propriétés de sécurité

Jour 2 (6h)

Analyse formelle de sécurité avec ProVerif

  • Le fonctionnement interne de ProVerif : ce qui se passe en coulisses
  • Comment éviter les erreurs de modélisation usuelles
  • Usage avancé : Prévenir les faux négatifs/attaques
  • Usage avancé : Éviter les cas de non-terminaison
  • Si le temps le permet : quelques notions avancées (restriction, secret fort, propriétés d’équivalence, confidentialité)

Étude de cas

  • Présentation étape par étape d’une étude de cas réelle. Nous examinerons l’ensemble du processus : de la lecture de la spécification à l’interprétation des résultats de l’analyse formelle.

Aperçu rapide de Tamarin

  • Aperçu de Tamarin et comparaison avec ProVerif
  • Comment transposer les concepts acquis à Tamarin

Intervenant(s)

  • Steve Kremer

    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

  • Lucca Hirschi

    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.

  • Jannik Dreier 

    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.

  • Alexandre Debant

    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.

Les prochaines sessions

2

Pour aller plus loin

À propos des tarifs

  • Tarif par personne : 1300 €
  • Partenariat avec le pôle Systematic et le pôle Aktantis : les entreprises membres du pôle bénéficient d’un tarif privilégié (-20% sur tarif de base) ;
  • Tarifs dégressifs à partir de 5 personnes (-10% de 5 à 9 inscrits, -20% plus de 10 inscrits) et en cas d’achat groupé des modules débutant et avancé (-20%) ;
  • Toutes les sessions en dehors de l’intra-entreprise se déroulent en distanciel.

Découvrir

Demander plus d'informations