next up previous
Next: Protocol Analysis Up: Using Non Interference for Previous: Protocol specification in SPA

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: 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{displaymath}
\begin{array}
{lll}
\lefteqn{Enemy\_1(e\_id,e\_nonce) \stack...
 ..._{id2},nonce,id1)).Enemy\_1(e\_id,e\_nonce)}\\ & & )\end{array}\end{displaymath}

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.


next up previous
Next: Protocol Analysis Up: Using Non Interference for Previous: Protocol specification in SPA