An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation

Author

Pironti, Alfredo ; Sisto, Riccardo

Author_Institution

Politecnico di Torino, Torino

fYear

2007

fDate

1-4 July 2007

Firstpage

839

Lastpage

844

Abstract

Spi2Java is a tool that enables semi-automatic generation of cryptographic protocol implementations, starting from verified formal models. This paper shows how the last version of spi2Java has been enhanced in order to enable interoperability of the generated implementations. The new features that have been added to spi2Java are reported here. A case study on the SSH transport layer protocol, along with some experiments and measures on the generated code, is also provided. The case study shows, with facts, that reliable and interoperable implementations of standard security protocols can indeed be obtained by using a code generation tool like spi2Java.

Keywords

Java; cryptographic protocols; formal verification; open systems; software tools; Spi2Java tool; automatic code generation; interoperable cryptographic protocol implementation; verified formal model; Calculus; Code standards; Cryptographic protocols; Cryptography; Electronic mail; Formal specifications; Java; Security; Testing; Transport protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Computers and Communications, 2007. ISCC 2007. 12th IEEE Symposium on

Conference_Location

Aveiro

ISSN

1530-1346

Print_ISBN

978-1-4244-1520-5

Electronic_ISBN

1530-1346

Type

conf

DOI

10.1109/ISCC.2007.4381508

Filename

4381508