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.
|