Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

Résumé Technique : Au-delà de la propriété de variante finie : Extension des modèles de groupes Diffie-Hellman symboliques

Énoncé du problème
Les groupes Diffie-Hellman (DH) sont fondamentaux pour les protocoles cryptographiques modernes, pourtant les vérificateurs de protocoles symboliques de pointe (tels que Tamarin, ProVerif et Maude-NPA) manquent d'un support complet pour leurs propriétés algébriques. Ces outils peuvent modéliser l'exponentiation et la multiplication des exposants, mais ils ne peuvent généralement pas modéliser la multiplication des éléments de groupe, ce qui correspond à l'addition des exposants. Cette limitation découle du fait que la théorie équationnelle décrivant les groupes DH complets (impliquant la distributivité, l'associativité et la commutativité) rend le problème d'unification indécidable et infini. Par conséquent, les outils existants ne peuvent pas raisonner sur des protocoles qui construisent des éléments de groupe composites (par exemple, le chiffrement ElGamal ou l'échange de clés MQV) où l'adversaire ou les parties honnêtes utilisent la structure de corps complète des exposants.

Méthodologie
Les auteurs proposent une procédure de semi-décision pour vérifier les propriétés de sécurité des protocoles utilisant la structure complète du groupe DH. L'approche intègre le raisonnement symbolique aux méthodes algébriques, implémentée comme une extension du prouveur Tamarin.

1. Fondement théorique : Ce travail s'appuie sur le système de réécriture proposé par Dougherty et Guttman, qui approxime les corps à l'aide d'un système de réécriture convergent ($\to_{DH}$) modulo associativité et commutativité (AC). Ce système permet la définition de formes normales pour les termes.
2. Hypothèse de non-annulation : L'approche repose sur deux conditions principales :
   • C1 : Tous les éléments de groupe appartiennent à un seul groupe fixe avec un générateur commun.
   • C2 (Non-annulation) : Les propriétés de sécurité impliquent des termes où les sous-termes ne s'annulent pas entre eux (c'est-à-dire qu'ils ne peuvent pas être réduits à l'élément identité 1 ou 0). Si cette condition échoue, l'outil peut toujours trouver des attaques valides, mais une preuve de sécurité nécessite une vérification manuelle pour s'assurer que les termes spécifiques ne s'annulent pas.
3. Résolution de contraintes hybride : L'innovation centrale est un algorithme de résolution de contraintes modifié qui évite l'unification directe pour les termes DH. Au lieu de cela, il emploie un processus en deux étapes :
   • Unification symbolique (Théorie simplifiée) : L'algorithme unifie d'abord les termes dans une théorie équationnelle simplifiée ($\varepsilon_{simp}$) qui exclut l'opérateur de multiplication de groupe. Cela permet d'utiliser les algorithmes d'unification existants de Tamarin pour faire correspondre les termes racines.
   • Reconstruction algébrique : Une fois les termes racines appariés, l'algorithme interprète les termes symboliques comme des objets algébriques (des polynômes sur un corps). Il classifie les exposants comme étant soit « fuis » (connus de l'adversaire), soit « secrets ». En utilisant l'élimination de Gauss (ou potentiellement l'algorithme de Buchberger pour les cas non linéaires), le système résout pour savoir si les exposants secrets peuvent être combinés avec les exposants fuis pour reconstruire le terme cible.
4. Fonction indicatrice : Pour déterminer si un terme est déductible, les auteurs définissent une fonction « indicateur ». Celle-ci identifie les composants secrets minimaux requis pour construire un terme. Si un indicateur ne peut pas être reconstruit à partir des connaissances de l'adversaire, le terme est jugé indéductible.
5. Modélisation de l'adversaire : L'extension supporte un adversaire actif de type Dolev-Yao capable d'appliquer tous les opérateurs DH. Le solveur de contraintes gère la déduction de l'adversaire en vérifiant si l'adversaire peut satisfaire les équations linéaires dérivées de l'interprétation polynomiale des termes.

Principales contributions

• Premier outil automatisé pour la théorie DH complète : Ce travail présente la première implémentation d'un outil de vérification automatisé capable de modéliser et de raisonner sur des protocoles utilisant la structure complète du groupe Diffie-Hellman, incluant la multiplication des éléments de groupe.
• Correction et complétude : Les auteurs prouvent que la relation de résolution de contraintes étendue est saine et complète (sous l'hypothèse de non-annulation). Si Tamarin trouve une attaque, il s'agit d'une exécution valide ; s'il prouve la sécurité, aucune exécution violante n'existe dans le modèle symbolique.
• Intégration avec Tamarin : L'approche est implémentée en modifiant l'algorithme de résolution de contraintes de Tamarin, en ajoutant de nouvelles règles ($C@, C_{Prem}, C=, C_{var}$) qui remplacent les règles d'unification standard pour les termes triés par DH par des étapes de résolution algébrique.
• Gestion des théories mixtes : La méthode supporte la combinaison de la théorie DH complète avec d'autres théories équationnelles définies par l'utilisateur (par exemple, le chiffrement symétrique, les paires) en « nettoyant » les termes combinés — en remplaçant les sous-termes DH par des variables fraîches pour l'unification, puis en réintroduisant les contraintes DH pour la résolution algébrique.

Résultats et études de cas
Les auteurs ont évalué l'implémentation sur plusieurs protocoles :

• Chiffrement ElGamal : L'outil a prouvé avec succès l'exécutabilité et la secretude du schéma de chiffrement ElGamal. Notamment, c'est la première fois qu'ElGamal est vérifié automatiquement dans le modèle symbolique avec un support DH complet. L'outil a également identifié correctement un manque de secret lorsque l'initiateur n'est pas authentifié.
• Échange de clés MQV : L'outil a été utilisé pour analyser le protocole MQV. Il a redécouvert avec succès l'attaque connue de « partage de clé inconnue » de Kaliski, démontrant la capacité de l'outil à trouver des attaques complexes impliquant des éléments de groupe composites.
• Évaluation de référence : L'extension a été testée sur 20 modèles Tamarin existants (incluant WireGuard et divers protocoles d'échange de clés) qui utilisaient auparavant une théorie DH restreinte. Les résultats ont montré que l'extension produit les mêmes verdicts de sécurité que la théorie restreinte pour ces protocoles, bien qu'avec un temps d'exécution accru dû à la complexité de l'espace de recherche étendu.

Signification
L'article affirme que ce travail représente une avancée significative dans la vérification de protocoles symboliques. En surmontant l'indécidabilité de l'unification dans les théories DH complètes, les auteurs permettent la vérification automatisée d'une classe plus large de protocoles cryptographiques qui reposent sur la structure algébrique complète des groupes Diffie-Hellman. La capacité de vérifier automatiquement ElGamal et de redécouvrir les attaques MQV en quelques minutes démontre la faisabilité, l'extensibilité et l'efficacité de l'approche, comblant ainsi le fossé entre les propriétés algébriques théoriques et l'analyse de sécurité automatisée pratique.