Skip to Main content Skip to Navigation
Reports

Strategy for Verifying Security Protocols with Unbounded Message Size

Yannick Chevalier 1 Laurent Vigneron 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a system for automatically verifying cryptographic protocols. This system, named Casrul, 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 provers in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in combination with Casrul in the European Union project AVISS (Automated Verification of Infinite State Systems). The aim of this paper is to describe the heart of Casrul: the model of the intruder behavior. It is based on a lazy strategy. Another advantage of our model is that it permits to handle parallel sessions and composition of keys. And for sake of completeness, we do not limit the number of sessions of the protocol to be run, nor the size of the messages sent. We have combined Casrul with the theorem prover daTac for successfully studying 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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072220
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:08:12 PM
Last modification on : Friday, March 12, 2021 - 5:16:03 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:59:02 PM

Identifiers

  • HAL Id : inria-00072220, version 1

Collections

Citation

Yannick Chevalier, Laurent Vigneron. Strategy for Verifying Security Protocols with Unbounded Message Size. [Research Report] RR-4368, INRIA. 2002, pp.18. ⟨inria-00072220⟩

Share

Metrics

Record views

143

Files downloads

242