UCT CS Research Document Archive

Generating Network Security Protocol Implementations from Formal Specifications

Tobler, Benjamin and Andrew Hutchison (2004) Generating Network Security Protocol Implementations from Formal Specifications. In Nardelli, Enrico, Sabina Posadziejewski and Maurizmo Talamo, Eds. Proceedings IFIP World Computer Congress - CSES 2004 2nd International Workshop on Certification and Security in Inter-Organizational E-Services, Toulouse, France.

Full text available as:
Postscript - Requires a viewer, such as GhostView
PDF - Requires Adobe Acrobat Reader or other PDF viewer.


We describe the Spi2Java code generation tool, which we have developed in an attempt to bridge the gap between formal security protocol specification and executable implementation. Implemented in Prolog, Spi2Java can input a formal security protocol specification in a variation of the Spi Calculus, and generate a Java code implementation of that protocol. We give a brief overview of the role of code generation in the wider context of security protocol development. We cover the design and implementation of Spi2Java which we relate to the high integrity code generation requirements identified by Whalen and Heimdahl. By defining a Security Protocol Implementation API that abstracts cryptographic and network communication functionality we show that protocol logic code can be separated from underlying cryptographic algorithm and network stack implementation concerns. The design of this API is discussed, particularly its support for pluggable implementation providers. Spi2Java's functionality is demonstrated by way of example: we specify the Needham-Schroeder Public Key Authentication Protocol, and Lowe's attack on it, in the Spi Calculus and examine a successful attack run using Spi2Java generated implementation of the protocol roles.

EPrint Type:Conference Paper
ID Code:153
Deposited By:Arnab, A
Deposited On:22 October 2004