Description
Nous présentons une méthode pour automatiser l'analyse des protocoles cryptographiques à partir de leurs descriptions sous forme de règles d'envoi de messages. Le problème de la détection d'attaque dans un environnement hostile se ramène à la résolution de contraintes sur un espace de messages. La résolution de ces contraintes implantée dans le logiciel issu du projet européen AVISPA est relativement efficace en pratique. Elle a permis de découvrir de nouvelles failles dans des protocoles en cours de standardisation; Nous décrivons une procédure de décision dans le cas d'un nombre fini de sessions avec des clés composées. L'approche s'étend au cas d'un intrus muni de règles de déduction pour prendre en compte des propriétés des primitives cryptographiques : comme le XOR ou l'exponentielle modulaire ...