Rule based programming in Java for protocol verification - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2004

Rule based programming in Java for protocol verification

Résumé

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.

Domaines

Autre [cs.OH]

Dates et versions

inria-00100025 , version 1 (26-09-2006)

Licence

Paternité

Identifiants

Citer

Horatiu Cirstea, Pierre-Etienne Moreau, Antoine Reilles. Rule based programming in Java for protocol verification. 5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, Narciso Marti-Oliet, 2004, Barcelona, Spain. 18 p, ⟨10.1016/j.entcs.2004.06.022⟩. ⟨inria-00100025⟩
162 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More