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 ...
Prochains exposés
-
CryptoVerif: a computationally-sound security protocol verifier
Orateur : Bruno Blanchet - Inria
CryptoVerif is a security protocol verifier sound in the computational model of cryptography. It produces proofs by sequences of games, like those done manually by cryptographers. It has an automatic proof strategy and can also be guided by the user. It provides a generic method for specifying security assumptions on many cryptographic primitives, and can prove secrecy, authentication, and[…]-
Cryptography
-