Protocol specification in SPA

 In this section we present a formalization of the Needham-Schroeder protocol using VSPA. Here we consider the reduced version of the protocol, omitting the public key requests by A and B . The formalization we give is very similar to the one in [Low96]. The main difference is in the language used (the CSP in that case). We are not interested in giving a new formalization of the protocol and of the enemy. The aim of this paper is to show a new technique to analyze the protocol based on NI-like properties. So the main difference with respect to [Low96] work can be found in the protocol analysis section (i.e., Section 6).

The reduced protocol is composed by the following three steps:

$$\begin{array} {llllll} & Message \ 1& A & \rightarrow & B: &... ...)\\ & Message \ 3 & A & \rightarrow & B: & PK_B(N_B)\end{array}$$

The protocol is modeled through two VSPA agents: the Initiator and the Responder. The Initiator accepts a user connection request, then starts the messages exchange with the Responder.

Protocol messages are all of the form:

$$msg\_i(mitt,dest,enc(key,p_1,p_2,\ldots, p_n))$$

where:

i is the message number (it ranges in [1 ...3]);

mitt is the identifier of the message sender;

dest is the identifier of the message addressee;

$enc(\ldots)$ is a generic public key encryption algorithm;

key is an encryption key;

$p_1, p_2, \ldots, p_n$ represents the information tuple conveyed by the (encrypted) message.

Besides protocol messages, there are some actions to allow interaction between users and the protocol.

A user $a\_id$ can make a connection request to $b\_id$ through action request(a_id,b_id). To inform users that the connection is established, the Initiator and the Responder give as output connection(a_id,b_id,ok) and r_connection(b_id,a_id,ok), respectively. In the case of a protocol failure the messages become: connection(a_id,b_id,no) and r_connection(b_id,a_id,no), respectively. Another action is executed by Responder to inform users that someone has made a connection request: r_running(a_id,b_id).
Initiator is defined using VSPA by:

$$\begin{array} {lll} Initiator(a\_id,a\_nonce) & \stackrel{\r... ...0.20in}\overline{connection}(a\_id,dest\_id,no).0\\ \end{array}$$

Initiator receives, through action $request(a\_id,dest\_id)$, a request from user a_id for a connection with user dest_id; then it starts a run of the protocol. It sends message 1 containing the sender identifier and its nonce, both encrypted with receiver's public key. When it receives message 2 containing the two nonces $a\_nonce^\prime$,dest_nonce encrypted with the Initiator public key, it checks if $a\_nonce^\prime$ is equal to the nonce sent in the first message ($a\_nonce$). If this is the case, it sends the other nonce $dest\_nonce$ to user $dest\_id$ and informs the user $a\_id$ that the connection with $dest\_id$ is established (action connection(a_id,dest_id,ok)). If the nonce $a\_nonce^\prime$ is different from $a\_nonce$, the protocol fails and this is notified through action $\overline{connection}(a\_id,dest\_id,no)$.

Similarly to Initiator, the Responder is defined in VSPA as follows:

$$\begin{array} {lll} Responder(b\_id,b\_nonce) & \stackrel{\r... ...0in}\overline{r\_connection}(b\_id,send\_id,no).0\\ \end{array}$$

Responder receives message 1, containing sender's nonce and identity (send_nonce,$send\_id^\prime$). It checks if the identifier contained in the plaintext part of the message (send_id) is equal to that contained in the ciphertext part. If it is so, it sends message 2 containing the nonce received and its own nonce, encrypted with the sender public key. It receives message 3 and checks if the nonce received is equal to its own; if the check is successful it informs, through the action $\overline{r\_connection}(b\_id,send\_id,ok)$, the user that the connection is established, otherwise it gives as output $\overline{r\_connection}(b\_id,send\_id,no)$ which represent an unsuccessful termination of the protocol. The complete protocol specification is defined as parallel composition of the agents described above:

$$\begin{array} {lll} Protocol & \stackrel{\rm def}{=} & (Initiator(a,na)\ \vert\ Responder(b,nb))\ \backslash \ L\end{array}$$

where $L = \{msg\_1, msg\_2, msg\_3\}$is the set of messages sent during the protocol.