HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Automated Unbounded Verification of Security Protocols

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 new model for automated verification of security protocols, permitting the use of an unbounded number of protocol runs. We prove its correctness, completeness and also that it terminates. It has been implemented and its efficiency is clearly shown by the number of protocols successfully studied. In particular, we present an attack previously unreporte- d on the Denning-Sacco symmetric key protocol.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072219
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:08:07 PM
Last modification on : Friday, February 4, 2022 - 3:23:32 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:58:56 PM

Identifiers

  • HAL Id : inria-00072219, version 1

Collections

Citation

Yannick Chevalier, Laurent Vigneron. Automated Unbounded Verification of Security Protocols. [Research Report] RR-4369, INRIA. 2002, pp.16. ⟨inria-00072219⟩

Share

Metrics

Record views

35

Files downloads

137