Vérification formelle du protocole d'échange de clé IKEv2

Defense type
Thesis
Starting date
End date
Room
IRISA Rennes, salle Metivier
Speaker
Tristan Ninet (TAMIS)
Theme

Dans cette thèse, nous analysons le protocole IKEv2 à l'aide de trois outils de vérification formelle : Spin, ProVerif et Tamarin. Pour effectuer l'analyse avec Spin, nous étendons une méthode existante de modélisation. En particulier, nous proposons un modèle de la signature numérique, du MAC et de l'exponentiation modulaire, nous simplifions le modèle d'adversaire pour le rendre applicable à des protocoles complexes, et nous proposons des modèles de propriétés d'authentification. Nos analyses montrent que l'attaque par réflexion, une attaque trouvée par une précédente analyse, n'existe pas. De plus, nos analyses avec ProVerif et Tamarin produisent de nouvelles preuves concernant les garanties d'accord non injectif et d'accord injectif pour IKEv2 dans le modèle non borné.

Nous montrons ensuite que la faille de pénultième authentification, une vulnérabilité considérée comme bénigne par les analyses précédentes, permet en fait d'effectuer un nouveau type d'attaque par déni de service auquel IKEv2 est vulnérable : l'Attaque par Déviation. Cette attaque est plus difficile à détecter que les attaques par déni de service classiques mais est également plus difficile à réaliser. Afin de démontrer concrètement sa faisabilité, nous attaquons avec succès une implémentation open-source populaire de IKEv2. Les contre-mesures classiques aux attaques DoS ne permettent pas d'éviter cette attaque. Nous proposons alors deux modifications simples du protocole, et prouvons formellement que chacune d'entre elles empêche l'Attaque par Déviation.

Composition of the jury
- Directeur de thèse : Stéphanie Delaune, Directrice de Recherche, CNRS, IRISA Rennes
Co-directeur de thèse : Olivier Zendra, Chargé de Recherche Inria Rennes
Rapporteur : Caroline Fontaine, Directrice de Recherche, CNRS, LSV / ENS Paris-Saclay
Rapporteur : Steve Kremer, Directeur de Recherche, Inria, LORIA Nancy
Examinateur : Thomas Genet, Maître de conférence, Université de Rennes 1
Examinateur : Pierre-Etienne Moreau, Professeur, Université de Lorraine, École des Mines de Nancy
Invité : Romaric Maillard, Architecte Equipements, Thales SIX GTS France