Title :
Spi2Java: automatic cryptographic protocol Java code generation from spi calculus
Author :
Pozza, Davide ; Sisto, Riccardo ; Durante, Luca
Author_Institution :
Dipt. di Automatica e Informatica, Politecnico di Turino, Torino, Italy
Abstract :
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 :
Java; cryptography; formal specification; process algebra; program compilers; protocols; specification languages; Java code generation; Spi2Java; cryptographic protocols; formal specification; parser analyzer; preprocessor analyzer; protocol flaw detection; security analyzer; specification language; spi calculus; Authentication; Calculus; Computer science; Computer security; Cryptographic protocols; Cryptography; Formal specifications; Java; Niobium; Risk analysis;
Conference_Titel :
Advanced Information Networking and Applications, 2004. AINA 2004. 18th International Conference on
Print_ISBN :
0-7695-2051-0
DOI :
10.1109/AINA.2004.1283943