Spi2Java

Spi2Java works with formal protocol models expressed in the spi-calculus. The methodology implied by Spi2Java is shown in Fig. 1. The user starts with a formally verified model of a security protocol (the model may have been verified using ProVerif). Then, supported by automatic tools, the user specifies some implementation details that are not captured by the formal model. When such details are ready in the eSpi document, an automatic tool generates the Java code that implements the protocol logic. Finally the user provides a manually written layer of functions for encoding and decoding data (the Encoding layer) which completes the protocol implementation. If the Encoding layer satisfies certain information flow properties, and certain other conditions are met, the Java implementation is guaranteed to satisfy (under the Dolev-Yao assumptions) the same security properties that hold on the original model. The details can be found in the most recent research papers. It is important to note that checking information flow properties is less critical than checking security properties in the Dolev-Yao model. However, the checking of information flow properties is not provided as part of the current version of Spi2Java.

Figure 1.

The Type System

Since Spi Calculus is an untyped language, while Java is statically typed, a type system for Spi Calculus has been designed (see Fig. 2), so that well typed Spi Calculus processes can be translated into Java programs.

Figure 2.

The Generated Code

Each Spi Calculus statement is translated into a sequence of Java statements, see Fig. 3. Thanks to formal translation rules and a formal simulation relation, the Java generated code can be proved to correctly refine the Spi Calculus process from which it was generated.

            /* let (xNa_7,xk1AB_7) = _w0_6 in */
            Nonce xNa_7 = (Nonce) _w0_6.getLeft();
            SharedKey xk1AB_7 = (SharedKey) _w0_6.getRight();

Visual Modelling

Spi calculus protocol models can be developed visually and the whole workflow can be managed seamlessly through a dedicated eclipse-based integrated development environment called Spi2JavaGUI, which includes the core Spi2Java.