Strategy for verifying security protocols with unbounded message size

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 protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. 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. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.