Rule based programming in Java for protocol verification

Horatiu Cirstea 1 Pierre-Etienne Moreau 1 Antoine Reilles 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents an approach for the development of model-checkers in a framework, called Tom, merging declarative and imperative features. We illustrate our method by specifying in Tom the Needham-Schroeder Public-Key protocol that aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. We describe the behavior of the agents exchanging messages as well as the intruders and the security invariants the protocol should verify using the rewrite rules of Tom. The (depth-first or breadth-first) exploration of the search space is described using the imperative features of the language. We propose several optimizations and we compare our results to existing approaches.
Type de document :
Communication dans un congrès
Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo. 5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, 2004, Barcelona, Spain, Elsevier, 18 p, 2004, Electronic Notes in Theoretical Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100025
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:25
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100025, version 1

Collections

Citation

Horatiu Cirstea, Pierre-Etienne Moreau, Antoine Reilles. Rule based programming in Java for protocol verification. Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo. 5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, 2004, Barcelona, Spain, Elsevier, 18 p, 2004, Electronic Notes in Theoretical Computer Science. 〈inria-00100025〉

Partager

Métriques

Consultations de la notice

232