Session executive education Apprentissage automatique, les briques technologiques pour les PME spéciale IA générative le 1er avril – GRATUIT !

Session deeptech Analyse des données de santé sensibles par l’apprentissage fédéré le 2 avril

Session état de l’art Cyberattaques dans les réseaux sans fils : quel impact, quels enjeux ? le 9 avril

Session état de l’art Les dispositifs médicaux intégrant de l’IA : challenges méthodologiques et règlementaires le 16 avril – NOUVEAU !

Session deeptech Scikit-learn, la boîte à outils de l’apprentissage automatique niveau 2 les 21 et 22 avril

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.

À l’issue de la formation, les participants seront en mesure de :

  • 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.

Public cible : ingénieurs et développeurs

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.

2
1600 / pers.

Aucune session disponible actuellement.

Contactez-nous

Témoignages

01

Très bonne formation ! Alliance de théorie et de pratique avec une réelle expertise et des retours « terrain » sur les bonnes pratiques et les erreurs à éviter.

Laurent GREMY

Senior researcher in Secure Transactions, Idemia

©️Inria

Pour aller plus loin

Informations pratiques

  • Durée : 2 jours (12h).
  • Horaires : 9h-12h / 13h30-16h30.
  • Délais d’accès : les inscriptions s’arrêtent 15 jours avant la date affichée.

  • Informations sur l’admission : l’admission au cours fait l’objet d’une sélection préalable. Le candidat doit répondre aux critères des pré-requis indiqués ci-dessus. 

  • Format : toutes les sessions en dehors de l’intra-entreprise se déroulent en distanciel. Cependant, si les participants sont localisés dans la même région, le format en présentiel pourrait être envisagé.

  • Modalités pédagogiques : la formation est délivrée en distanciel, en langue française avec les supports en anglais. Le cours peut se dérouler en anglais si tous les participants sont anglophones. La taille du groupe : 12 personnes maximum.

  • Privatisation du module (session intra-entreprise) : à partir de 5 personnes. Nous contacter via le formulaire de contact.

  • Moyens pédagogiques : le support du cours sera fourni aux participants.

  • Modalités d’évaluation et de suivi : l’évaluation est assurée par les quizz. Une attestation de formation est délivrée à la fin du parcours.

  • Accessibilité – handicap : Inria s’engage à garantir l’accessibilité de ses formations à distance et en présentiel aux personnes en situation de handicap. Plus de détails

 

À propos des tarifs

  • Tarif : 1600 € par participant 
  • Tarifs dégressifs à partir de 5 personnes (-10% de 5 à 9 inscrits, -20% plus de 10 inscrits)
  • Tarif dégressif pour les entreprises membres du pôle Aktantis (-20%)
  • Modalités de financement : fonds propres

Découvrir

Demander plus d'informations