Formal verification of the Internet Key Exchange (IKEv2) security protocol

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

Tristan Ninet (1, 2)

1 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
2 TAMIS - Threat Analysis and Mitigation for Information Security

In this thesis, we analyze the IKEv2 protocol specification using three formal verification tools: Spin, ProVerif and Tamarin. To perform the analysis with Spin, we extend and improve an existing modeling method with a simpler adversary model and a model for common cryptographic primitives and Lowe's authentication properties. As a result we show that the reflection attack, an attack found by a previous analysis, is actually not applicable. Moreover, our analysis using ProVerif and Tamarin provides new results regarding non-injective agreement and injective agreement guaranties of IKEv2 in the unbounded model. We then show that the penultimate authentication flaw, a vulnerability that was considered harmless by previous analyses, actually allows for a new type of Denial-of-Service attack, which works against IKEv2: the Deviation Attack. The Deviation Attack is harder to detect than existing DoS attacks, but is also harder to perform. To concretely demonstrate the attack, we successfully implement it against a popular open-source implementation of IKEv2. Finally, we study the use of existing DoS countermeasures and existing configuration options to defeat the attack, but we only find mitigations or incomplete workarounds. We therefore tackle the problem at a higher level: we propose two possible inexpensive modifications of the protocol, and formally prove that they both prevent the attack.

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.

Mots clés: Cryptographic protocol; Formal verification; IKEv2; Denial-Of-Service

Mots clés: Protocole cryptographique; Vérification formelle; IKEv2; Déni de service

Domaines: Cryptographie et sécurité [cs.CR]

Tristan Ninet. Formal verification of the Internet Key Exchange (IKEv2) security protocol. Cryptography and Security [cs.CR]. Université Rennes 1, 2020. English. ⟨NNT : 2020REN1S002⟩. ⟨tel-02882167⟩