UCT CS Research Document Archive

Generation, Analysis and Verification of Cryptographic Protocol Implementations

Tobler, Ben and ACM Hutchison (2003) Generation, Analysis and Verification of Cryptographic Protocol Implementations. In Eloff, JHP, HS Venter, L Labuschagne and MM Eloff, Eds. Proceedings 3rd annual Information Security South Africa Conference, pages 297-306, Sandton Convention Centre, Sandton, South Africa.

Full text available as:
PDF - Requires Adobe Acrobat Reader or other PDF viewer.


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.

EPrint Type:Conference Paper
Keywords:code generation, cryptographic protocol, cryptographic protocol analysis, network security
ID Code:121
Deposited By:Arnab, A
Deposited On:11 May 2004
Alternative Locations:http://www.cs.uct.ac.za/Research/DNA/resources/publications_repository/tobler2003_GenerationAnalysisVerificationCrypto.pdf