JavaSPI is a model-driven development framework for security protocols and distributed security-aware applications, characterized by having Java not only as the target implementation language for protocols and applications but also as the modeling language. JavaSPI works in a way similar to Spi2Java, the main differences being the modeling language (Java in this case) and the way extra refinement information is attached to the model (by Java annotations in this case). As with Spi2Java, the outcome of the development process is an interoperable implementation of the modeled protocol or application.
The JavaSPI workflow is depicted in Figure 1.
Initially, the protocol (or application) is defined abstractly by specifying its Dolev-Yao model in Java, by means of a dedicated library called SpiWrapperSim. This library also enables the simulation of the symbolic model (which is obtained simply by executing the Java code of the model inside any Java IDE). One interesting aspect of this choice is that the debugging facilities already available for the Java language automatically support interactive simulation of these models (for example, enabling step-by-step execution).
Once the model has been developed and validated by simulation, it can be annotated in order to specify additional implementation choices. Then, the annotated model can be converted into an equivalent proverif source that can be used for formal verification. After having formally verified the model, the last step is code generation, which is done by interpreting the annotations in the model and turning the model into a real interoperable application, according to the information found in the annotations. The concrete implementation is based on the same library (SpiWrapper) used by Spi2Java. Hence, in a similar way, the hand-written implementation of the encoding layer is necessary in order to complete the protocol or application code.