Contribuez à SecuObs en envoyant des bitcoins ou des dogecoins.
Nouveaux articles (fr): 1pwnthhW21zdnQ5WucjmnF3pk9puT5fDF
Amélioration du site: 1hckU85orcGCm8A9hk67391LCy4ECGJca

Contribute to SecuObs by sending bitcoins or dogecoins.



Maude-NPA facilite l'analyse des protocoles cryptographiques

Par Rédaction, secuobs.com
Le 27/03/2009


Résumé : Maude-NPA est une plateforme d'outils facilitant l'analyse semi-automatique des protocoles cryptographiques. Des exemples sont fournis dans le manuel d'utilisation avec les protocoles Needham-Schroeder à clé publique, eXclusive-OR et Diffie-Hellman.



Maude-NPA, ou Maude-NRL Protocol Analyser, est un ensemble d'outils d'analyse pour les protocoles cryptographiques. Il prend en compte un plus grand nombre de propriétés algébriques des crypto-systèmes que n'importe quel autre outil existant dans ce domaine. Basé sur Maude ( lien ), il inclut notamment l'annulation des chiffrements/déchiffrements, mais aussi les groupes abéliens ( lien ) avec eXclusive-OR ( XOR - lien ) et les exposants ( lien ) pour le calcul de grandes puissances entières.

Maude-NPA se base concrètement sur une approche utilisant conjointement l'unification et les recherches inverses qui sont effectuées depuis un état final pour déterminer l'accessibilité par une attaque. Maude-NPA implémente plus spécifiquement des théories de réécriture logique et de rétrécissement vers des ensembles minimalistes de solutions à tester. Il offre dans le même temps un support plus large des théories de résolution des systèmes d'équations en incluant notamment les théories associatives-commutatives ( AC - lien ) pour faciliter la déduction automatique.

Un manuel d'installation/utilisation est disponible ( lien ), il inclut de nombreux exemples pour différents protocoles afin d'aider à la compréhension des processus d'analyse. Sont également exposées les fondations formelles des réécritures logiques et les optimisations appliquées ici afin d'augmenter les performances de déduction par réduction des espaces de recherche. A noter que pour utiliser Maude-NPA 1.0 ( lien ), il est impératif d'avoir préalablement une installation fonctionnelle de Maude en version 2.4 ( lien ).

On retrouve notamment dans le manuel les mécanismes de chargement et de spécification des protocoles ainsi que la syntaxe avec un exemple concret portant sur le protocole Needham-Schroeder à clé publique ( NSPK - lien ), protocole qui servira par la suite à présenter différentes commandes. On notera également l'énumération des théories supportées pour la résolution des systèmes d'équations, puis la présentation des outils mis à disposition via deux exemples pratiques, XOR et Diffie-Hellman ( lien ), impliquant les théories AC citée précédemment.

Les limitations actuelles de Maude-NPA et le plan de développement pour les extensions à venir sont finalement introduits, alors qu'une page de démonstration est disponible directement en ligne ( lien ) via une interface Web permettant de s'assurer des capacités fonctionnelles de l'analyseur sous-jacent qu'elle interface.

Source : Security Circus ( lien )