Strategy for Verifying Security Protocols with Unbounded Message Size

Yannick Chevalier 1 Laurent Vigneron 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The generated rewrite rules can be used for detecting flaws with various systems. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size.
Type de document :
Article dans une revue
Journal of Automated Software Engineering, Springer, 2004, 11 (2), pp.141-166
Liste complète des métadonnées

https://hal.inria.fr/inria-00099945
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:12:48
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00099945, version 1

Citation

Yannick Chevalier, Laurent Vigneron. Strategy for Verifying Security Protocols with Unbounded Message Size. Journal of Automated Software Engineering, Springer, 2004, 11 (2), pp.141-166. 〈inria-00099945〉

Partager

Métriques

Consultations de la notice

204