Specifying Authentication Protocols Using ELAN

Horatiu Cirstea 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Programming with rewrite rules and strategies has been already used for describing several computational logics. In this paper is described the way the Needham-Schroeder Public-Key protocol is specified in ELAN, the system developed in Nancy for executing rewrite programs. The protocol aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. The protocol has been shown vulnerable and a correction has been proposed by G. Lowe. The behavior of the agents and of the intruders as well as the security invariants the protocol should verify are naturally described by conditional rewrite rules. The application of the rewrite rules is controlled by strategies. Similar attacks to those already described in the literature have been discovered. We show how different strategies using the same set of rewrite rules can improve the efficiency in finding the attacks and we compare our results to existing approaches.
Document type :
Conference papers
Complete list of metadatas

Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 9:10:40 AM
Last modification on : Thursday, January 11, 2018 - 6:19:57 AM
Long-term archiving on : Wednesday, March 29, 2017 - 12:57:50 PM


  • HAL Id : inria-00107815, version 1



Horatiu Cirstea. Specifying Authentication Protocols Using ELAN. Workshop on Modelling & Verification, Dec 1999, Besançon, France, 17 p. ⟨inria-00107815⟩



Record views


Files downloads