Loading...
Please wait, while we are loading the content...
Similar Documents
Generating network security protocol implementations from formal specifications.
| Content Provider | CiteSeerX |
|---|---|
| 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. Initially we discuss the role of code generation in the wider context of security protocol design and development. We cover the design and implementation of Spi2Java which we relate to the high integrity code generation requirements identified by Whalen and Heimdahl. We show that by defining a Security Protocol Implementation API that abstracts cryptographic and network communication functionality, protocol logic code can be separated from underlying cryptographic algorithm and network stack implementation concerns. The design of this API is also discussed, particularly its support for pluggable implementation providers. Spi2Java’s functionality is demonstrated by way of example: we specify the Needham- Schröeder 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. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Network Stack Implementation Concern Executable Implementation Pluggable Implementation Provider Formal Security Protocol Specification Successful Attack Run Spi Calculus Needham Schr Wider Context High Integrity Code Generation Requirement Security Protocol Implementation Api Formal Specification Code Generation Spi2java Code Generation Tool Network Security Protocol Implementation Protocol Role Public Key Authentication Protocol Java Code Implementation Security Protocol Design Spi2java Functionality Cryptographic Algorithm Network Communication Functionality Protocol Logic Code |
| Content Type | Text |
