Vérification automatique de protocoles cryptographiques avec CASRUL

Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Les protocoles cryptographiques sont utilisés pour protéger l'accès aux systèmes informatiques et les transactions sur les réseaux. l'expérience a montré que la conception de tels protocoles est souvent erronée, meme en admettant que la cryptographie est parfaite, autrement dit qu'un message codé ne peut se décrypter sans la clé. Un environnement hostile peut intercepter, analyser et modifier les messages échangés. Si le protocole est mal concu, l'adversaire peut sans cryptanalyse mais en choisissant convenablement les substituts de messages obtenir des informations secrètes. La possibilité de telles attaques est difficile à déterminer car le nombre de sessions de protocoles et le nombre de messages possibles a priori est infini. Néanmoins par une analyse formelle et des outils automatiques comme CASRUL, qui est l'objet de notre exposé, il est possible de révéler ces failles.
Type de document :
Communication dans un congrès
Journées Systèmes et Logiciels Critiques, 2001, Grenoble, France, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00100559
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:47:34
Dernière modification le : mercredi 25 juillet 2018 - 01:23:46

Identifiants

  • HAL Id : inria-00100559, version 1

Collections

Citation

Michaël Rusinowitch. Vérification automatique de protocoles cryptographiques avec CASRUL. Journées Systèmes et Logiciels Critiques, 2001, Grenoble, France, 2001. 〈inria-00100559〉

Partager

Métriques

Consultations de la notice

84