Protocol Analysis

 In order to test the protocol correctness we consider the parallel composition of all the agents described so far. As we are considering the network as insecure, the right way to compose the Enemy with the partners of the protocol is exactly on the communication channel between the Initiator and the Responder. This means that the Enemy is composed in parallel with them inside the scope of the restriction operator.

We want to reduce the problem of testing if the protocol correctly authenticates the two users to a problem of information flow control between two levels. For this reason the process actions have been divided into high and low level actions (sets $Act_H$ and $Act_L$). Since we want to check the influence that an intruder can have on the protocol execution, $Act_H$ is composed by the action fake, which is executed at every Enemy iteration and so can be seen as an abstraction of the Enemy activity. All the other actions belong to the low level.

$$\begin{array} {lll} Protocol & \stackrel{\rm def}{=} & (Init... ...onder(b\_id,nb)\ \vert\ Enemy(e,ne))\ \backslash \ L\end{array}$$

where:

-

L = {msg_1, msg_2, msg_3}

-

$Act_H$ = {fake}

-

$Act_L$ = {msg_1, msg_2, msg_3, request, r_running, connection, r_connection}

Since we want to focus on the ``correct'' execution of the protocol, we consider, for the analysis, only the actions representing the start and the correct termination of a session between $a\_id$ and $b\_id$:

$$request(a\_id,b\_id),\ connection(a\_id,b\_id,ok),\ r\_connection(b\_id, a\_id,ok).$$

All the other actions are hidden. So, we define process Protocol' as follows:

$$Protocol' \stackrel{\rm def}{=}Protocol / \{ \begin{array}[t... ...d, ok), \\ r\_connection(any\_id, any\_id', no) \ \}\end{array}$$

The security property we automatically check is SNNI, which is equal to NDC. The tool used for this analysis is the Compositional Security Checker (CoSeC), a semantic-based tool for the automatic verification of some compositional information flow properties [FG96,FG].

In particular, using CoSeC, we check if the following holds:

$$Protocol' \backslash fake \approx_T Protocol'/fake$$

As we said above, the action fake represents the Enemy activity. So we can see $Protocol' \backslash fake$ as the protocol on a completely secure channel (i.e., with no enemies), and Protocol'/fake as the protocol under the Enemy attack. If these two processes are not equivalent we can conclude that the Enemy is able to interfere with the correct execution of the protocol.

The automatic check gives the following answer:

false
Agent Protocol'/fake
can perform action sequence 'r_connection_b_a_ok
which agent Protocol'$\setminus$fake
cannot

where action $'r\_connection\_b\_a\_ok$ corresponds to $r\_connection(b\_id, a\_id , ok)$ in VSPA. This answer means that the high level action fake (and so the enemy) interferes with the low level actions, i.e., with the correct execution of the protocol. In particular we see that when we hide the fake action, and so we permit the enemy to operate indiscriminately, we obtain an execution sequence where B is convinced to communicate to A (action $'r\_connection\_b\_a\_ok$) but A has never started the protocol with B . Since when we restrict action fake (we do not allow any activity of the Enemy ) we do not have this particular execution of the protocol, we can conclude that the enemy is able to force an anomalous behaviour of the protocol. If we study the labelled transition system generated by the initial process Protocol looking for a trace with a $r\_connection(b\_id, a\_id , ok)$ and without a $request(a\_id, b\_id)$, we find out the following sequence corresponding to a specific attack:

$$request(a\_id,e\_id), r\_running(a\_id,b\_id), connection(a\_id,e\_id,ok), r\_connection(b\_id, a\_id , ok)$$

This means that user B is convinced to have established a connection with user A , while A has made a request to user E : hence, the enemy has cheated B .

To realize the cheat, two runs have to be active at the same time: one between the users A and E , and one between the users E (the intruder that claims to be A ) and B . Using $\alpha$ and $\beta$ to indicate the two runs, the sequence that allows to cheat is:

$$\begin{array} {llll} Message\ \alpha1. & A \rightarrow E & :... ...essage\ \beta3. & E(A) \rightarrow B & : & PK_B(N_B)\end{array}$$

In message $\alpha1$, A sends his nonce and identifier to E , trying to establish a connection with him. When E receives this message, (s)he forwards it to B , pretending to be A ($\beta1$). B accepts the message and sends back his nonce and the nonce just received ($\beta2$). E intercepts this message and, since he cannot decrypt it, he uses A as an oracle forwarding to him the massage ($\alpha2$). A accepts and decrypts it; then he sends to E the last message containing $N_B$ ($\alpha3$), considering established the session with E . In this way E has learn B 's nonce: then he can send it back to B ($\beta3$), that thinks to have just established a session with A .

The problem is in message 2 of the protocol that contains the two nonces. Since there is no identifier in it, anyone can intercepts and forwards it claiming to be anyone else.

The correct version of the protocol is:

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

Where message 2 now contains also the sender identifier.

Using again SC to analyze the corrected formalization, we can see that now the agent Protocol' satisfies the SNNI property, so we can conclude that Enemy is not able to interfere with the protocol.

The formalization used so far presents some limitations. For example, only one session can be established. In [Ghe97] it has been studied an improved model which allows the execution of multiple sessions. Another possible extension of the model is related to the equivalence notion used in the analysis. Trace equivalence is not able to detect deadlocks. In [Ghe97] this protocol has been analyzed also with respect to a stronger equivalence notion (bisimulation equivalence) which is able to detect the presence of deadlocks.