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.

An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation / Pironti, Alfredo; Sisto, Riccardo. - STAMPA. - (2007), pp. 839-844. (Intervento presentato al convegno IEEE Symposium on Computers and Communications (ISCC 07) tenutosi a Aveiro, Portugal nel 1-4 July 2007) [10.1109/ISCC.2007.4381508].

An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation

PIRONTI, ALFREDO;SISTO, Riccardo
2007

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.
2007
9781424415205
File in questo prodotto:
File Dimensione Formato  
iscc07_author_postprint.pdf

accesso aperto

Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 167.03 kB
Formato Adobe PDF
167.03 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1659069
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo