The Attacker

 In order to analyze the protocol it is necessary to study its behaviour when it is attacked by a malicious user. This intruder can be a normal user of the computer network that has decided to assume an incorrect behaviour. In particular we want to model a typical ``man-in-the-middle'' attack. So the intruder is able to:

• intercept any sent message;
• hold or forward any intercepted messages, possibly changing plaintext parts, even if he does not understand the contents of the encrypted part;
• decrypt messages encrypted with his own public key; we assume that the encryption algorithm used is secure, so the enemy can decrypt only the messages which are encrypted with his own public key;
• introduce new messages into the system (using informations he knows).

In order to simplify the specification we do not consider the possibility of storing intercepted information for later uses. In particular the enemy is able to use only the information gained in the last intercepted message when (s)he introduces new messages in the system. This is different from what is done in [Low96] where the enemy has a local memory where (s)he can store stolen information and reuse it later. We could define this more complex enemy also in our model but we prefer to use the simpler version with no memory which is sufficient for this analysis.

First, we present the enemy activity for message 1 and then we will see the whole Enemy agent. We have inserted C-like comments in order to better explain what is going on.

$$\begin{array} {lll} \lefteqn{Enemy\_1(e\_id,e\_nonce) \stack... ..._{id2},nonce,id1)).Enemy\_1(e\_id,e\_nonce)}\\ & & )\end{array}$$

where $I_{id}$ and $R_{id}$ are the sets of all the possible initiators and responder identifiers, respectively. We have an analogous situation for messages 2 and 3. So the VSPA specification for the Enemy is given by the following agent:

$$\begin{eqnarray*} \lefteqn{Enemy(e\_id,e\_nonce) \stackrel{\rm def}{=}} \\ & & f... ...nce)).Enemy(e\_id,e\_nonce)} $}\\ & & \hspace*{0.20in}) \\ & & ) \end{eqnarray*}$$

The aim of the action fake will be explained later. As for the other agents, the Enemy parameters are the intruder's identifier and nonce.