Generating Network Security Protocol Implementations from Formal Specifications

Tobler, Benjamin and Hutchison, Andrew (2004) Generating Network Security Protocol Implementations from Formal Specifications, Proceedings of IFIP World Computer Congress - CSES 2004 2nd International Workshop on Certification and Security in Inter-Organizational E-Services, 26 - 27 August 2004, Toulouse, France, Kluwer Academic Publisher.

	Postscript tobler04.ps Download (0B)
	PDF tobler04.pdf Download (316kB)

Abstract

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.

Item Type:	Conference paper
Date Deposited:	22 Oct 2004
Last Modified:	10 Oct 2019 15:35
URI:	http://pubs.cs.uct.ac.za/id/eprint/153

Actions (login required)

View Item