Wireless Authentication in $\chi$-Spaces

Federico Crazzolara
Giuseppe Milicia

February 2003

Abstract:

The $\chi$-Spaces framework provides a set of tools to support every step of the security protocol's life-cycle. The framework includes a simple, yet powerful programming language which is an implementation of the Security Protocol Language (SPL). SPL is a formal calculus designed to model security protocols and prove interesting properties about them. In this paper we take an authentication protocol suited for low-power wireless devices and derive a $\chi$-Spaces implementation from its SPL model. We study the correctness of the resulting implementation using the underlying SPL semantics of $\chi$-Spaces

Available as PostScript, PDF.

Last modified: 2003-06-08 by webmaster.