Copyright Notice:
The publication copies distributed in this site are
provided to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders (as explicitly indicated). All persons copying
this information are expected to adhere
to the terms and constraints invoked by each copyright. In
most cases, these works may not be reposted without the explicit
permission of the copyright holder
Alfredo Pironti, Riccardo Sisto,
An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation,
in ISCC 2007 - 12th IEEE Symp. on Computers and Communications, Aveiro, Portugal, July 2007, IEEE, pp. 839-844.
©2007 IEEE
doi: 10.1109/ISCC.2007.4381508
PDF
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
Back to Riccardo Sisto's publications