Compiling and Verifying Security Protocols

Florent Jacquemard 1 Michaël Rusinowitch 1 Laurent Vigneron
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a direct and fully automated translation from standard security protocol descriptions to rewrite rules. This compilation defines non-ambiguous operational semantics for protocols and intruder behavior: they are rewrite systems executed by applying a variant of ac-narrowing. The rewrite rules are processed by the theorem-prover DATAC. Multiple instances of a protocol can be run simultaneously as well as a model of the intruder (among several possible). The existence of flaws in the protocol is revealed by the derivation of an inconsistency. Our implementation of the compiler CASRUL, together with the prover DATAC, permitted us to derive security flaws in many classical cryptographic protocols.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072712
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:40:57 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Long-term archiving on : Sunday, April 4, 2010 - 8:43:45 PM

Identifiers

  • HAL Id : inria-00072712, version 1

Collections

Citation

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron. Compiling and Verifying Security Protocols. [Research Report] RR-3938, INRIA. 2000, pp.25. ⟨inria-00072712⟩

Share

Metrics

Record views

154

Files downloads

297