Specifying Authentication Protocols Using Rewriting and Strategies

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. This paper describes the way the Needham-Schroeder Public-Key protocol is specified in \elan, the system developed in Nancy to model and compute in the rewriting calculus. 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 to be vulnerable and a correction has been proposed. 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 whose application 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.
Type de document :
Communication dans un congrès
Third International Workshop on Practical Aspects of Declarative Languages - PADl'01, Mar 2001, Las Vegas, Nevada, USA, 15 p, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00100509
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:46:23
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100509, version 1

Collections

Citation

Horatiu Cirstea. Specifying Authentication Protocols Using Rewriting and Strategies. Third International Workshop on Practical Aspects of Declarative Languages - PADl'01, Mar 2001, Las Vegas, Nevada, USA, 15 p, 2001. 〈inria-00100509〉

Partager

Métriques

Consultations de la notice

148