Automated Unbounded Verification of Security Protocols

Yannick Chevalier (1) , Laurent Vigneron (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

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.

Mots clés: security protocols; verification; lazy strategy; unbounded runs

Domaines: Autre [cs.OH]

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