Developing security protocols in χ-Spaces

It is of paramount importance that a security protocol effectively enforces the desired security requirements. The apparent simplicity of informal protocol descriptions hides the inherent complexity of their interactions which, often, invalidate informal correctness arguments and justify the effort of formal protocol verification. Verification, however, is usually carried out on an abstract model not at all related with a protocol’s implementation. Experience shows that security breaches introduced in implementations of successfully verified models are rather common. The χ-Spaces framework is an implementation of SPL (Security Protocol Language), a formal model for studying security protocols. In this paper we discuss the use of χ-Spaces as a tool for developing robust security protocol implementations. To make the case, we take a family of key-translation protocols due to Woo and Lam and show how χ-Spaces aids several steps in the development of a security protocol – protocol executions can be simulated in hostile environments, a security protocol can be implemented, and security properties of implementations can be formally verified