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 preprocessor, 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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Avalle, Matteo; Pironti, Alfredo; Sisto, Riccardo: Formal verification of security protocol implementations: a survey (2014)
- Pironti, Alfredo; Sisto, Riccardo: Safe abstractions of data encodings in formal security protocol models (2014)
- Simonsen, Kent Inge Fagerland; Kristensen, Lars M.; Kindler, Ekkart: Generating protocol software from CPN models annotated with pragmatics (2013)
- Blanchet, Bruno: Security protocol verification: symbolic and computational models (2012)
- Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen: Verified interoperable implementations of security protocols (2007)