Spi2Java: Automatic Cryptographic Protocol Java Code Generation from spi calculus

The aim of this work is to describe a tool (Spi2Java) that automatically generates Java code implementing cryptographic protocols described in the formal specification language spi calculus. Spi2Java is part of a set of tools for spi calculus, also including a pre-processor, a parser, and a security analyzer. The latter can formally analyze protocols and detect protocol flaws. When a protocol has been analyzed and an adequate confidence about its correctness has been reached, Spi2Java can generate a corresponding correct Java implementation of the protocol, thus dramatically reducing the risk of introducing security flaws in the coding phase.

• Type: Conference
• Year: 2004
• Where: AINA
• Authors: Davide Pozza, Riccardo Sisto, Luca Durante
• Keywords: AINA 2004, Computer Networks, Language Spi Calculus, Protocol Flaws, Spi Calculus