Parcours IL / Orientation IL,MFLS & Parcours SIS / Orientation SIRAV
Les protocoles cryptographiques sont des programmes visant à sécuriser les communications digitales sur des réseaux ouverts comme Internet. Les exemples de protocoles sont nombreux : protocoles de paiement par carte bancaire, établissement d’un canal sécurisé (par exemple TLS sous-jacent à HTTPS), protocoles de vote électronique, etc. D’apparence simple, ils sont notoirement difficiles à concevoir et les bonnes pratiques actuelles imposent de les vérifier via des analyses formelles rigoureuses.
Ce cours présentera des méthodes de modélisation et d’analyse formelle pour des protocoles cryptographiques, basées sur des techniques de déduction automatique et de résolution de contraintes. Nous apprendrons aussi à utiliser un outil d’analyse dédié, tel que ProVerif. Cela pourra prendre la forme d’une mini-compétition entre élèves pour concevoir le protocole le plus robuste et trouver des failles et attaques dans les autres protocoles.
Prérequis
Connaissances de base en logique.
Acquis d’apprentissage
- Gérer et surveiller le système d’information (connaissance des protocoles, detection de flux malveillants, journalisation, gestion des politiques de sécurité) B1C1
- Vérifier la sécurité du SI (confidentialité, authentification, intégrité, disponibilité, traçabilité et non répudiation) B1C5
- Fonctionnement de différents protocoles (TLS, protocoles de vote électroniques, etc.)
- Exemples d’attaques sur ces protocoles et leur impact.
- Fondations logiques : Algèbre de termes, théorie équationnelle, clauses de Horn et procédures de résolution.
- Apprentissage et utilisation d’un langage formel pour la modélisation des protocoles via l’utilisation d’un outil de preuve dédié.
- Concevoir et analyser des protocoles cryptographiques pour les prouver sûr ou trouver des attaques.
Compétences visées
- Concevoir, modéliser et d’analyser des protocoles cryptographiques à l’aide d’outils dédiés tels que ProVerif.
- Gérer et surveiller le système d’information (connaissance des protocoles, détection de flux malveillants, journalisation, gestion des politiques de sécurité)
- Vérifier la sécurité du SI (confidentialité, authentification, intégrité, disponibilité, traçabilité et non répudiation)
- Concevoir et développer des systèmes logiciels sûrs et sécurisés
- Intégrer des méthodes et techniques formelles de modélisation, d’analyse, de vérification et de validation dans le processus de développement de logiciels critiques.
Parcours IL / Orientation IL,MFLS & Parcours SIS / Orientation SIRAV