Spi2Java and JavaSPI are model driven development (MDD) frameworks for implementing security protocols in Java. In these frameworks, the MDD paradigm is combined with formal methods in order to produce protocol implementations with high security confidence. Both frameworks are based on symbolic formal protocol models in the Dolev-Yao style. By analysing these models many kinds of logical flaws can be detected and the models can be proved to fulfill their intended security properties. Once confidence in model correctness has been reached, the models can be semi-automatically refined into Java interoperable implementations, with the guarantee that certain Dolev-Yao security properties are preserved in the final implementation. This is a first step towards bridging the gap between the verified abstract formal models, and their concrete implementations.
The original framework (Spi2Java) was based on a textual specification language called spi-calculus for specifying protocol models. Later on, a graphical specification notation for protocol models and an eclipse-based graphical user interface (Spi2JavaGUI) were added to Spi2Java, for visual modeling and seamless development. Another effort in the direction of simplifying the use of Spi2Java for Java experienced developers was the creation of JavaSPI, which is a framework similar to Spi2Java where spi-calculus models are expressed using the Java programming language, with the aid of a dedicated set of library classes.
Spi2Java, Spi2JavaGUI and JavaSPI have been designed and developed at Politecnico di Torino, Italy, in Prof. Sisto's research group. They are currently maintained at Politecnico di Torino, Italy by:
Former participants: