Generation, Analysis and Verification of Cryptographic Protocol Implementations

Tobler, Ben and Hutchison, ACM (2003) Generation, Analysis and Verification of Cryptographic Protocol Implementations, Proceedings of 3rd annual Information Security South Africa Conference, 9 - 11 July, Sandton Convention Centre, Sandton, South Africa, 297-306, ISSA.

[img] PDF

Download (39kB)


Network security is an area of increasing importance in commercial, public and private environments. Much research has been done in the area of design and analysis of the cryptographic protocols that provide this security. However, there has been little focus on research into the correctness of the implementations of these protocols, as is evidenced by the number of security flaws found in implementations of cryptographic protocols in commercial software systems on a regular basis. In this research project we investigate the development of a code generation tool for generating protocol implementations that can be proven to meet their specifications. Requirements for generating such high integrity code involve using a cryptographic protocol specification language that has formal semantics, ideally a target implementation language that also has formal semantics and a translation process between the two that is proven to preserve the meaning of the specification in the mapping to the implementation. The ability to automatically generate protocol implementations from their specifications will also facilitate analysis such as comparing the performance of protocols with the same goals and testing the scalability of protocols for secure group communication, as well verification of other existing implementations of protocols.

Item Type: Conference paper
Uncontrolled Keywords: code generation, cryptographic protocol, cryptographic protocol analysis, network security
Alternate Locations:
Date Deposited: 11 May 2004
Last Modified: 10 Oct 2019 15:36

Actions (login required)

View Item View Item