Related work

 The Needham-Schroeder public key protocol has been considered in many papers as an example to illustrate protocol analysis techniques and tools.

In [Low96] it is presented an analysis method based on the FDR tool and CSP [Hoa85] language. The FDR tool takes as input a CSP specification and a CSP implementation and verifies if the latter refines the former. In order to test if the protocol achieves mutual authentication, the author splits the problem in two: (i) test if the protocol authenticates the responder; (ii) test if the protocol authenticates the initiator.

In our model we can make an analogous check: it is sufficient to test if the security property SNNI is satisfied by the process Protocol where the visible actions are composed by the pair:

(i)

r_running(a_id,b_id), connection(a_id,b_id,ok) for the responder authentication;

(ii)

request(a_id,b_id), r_connection(b_id, a_id,ok) for t he initiator authentication.

As in [Low96] we obtain that the protocol fails in the initiator authentication, since we can have $r\_connection(b\_id, a\_id , ok)$ without $request(a\_id, b\_id)$. But unlike [Low96], our model allows to consider more than two actions at the same time. In this way it is possible to test if the protocol achieves mutual authentication with only one check.

Moreover we observe that the (i) check is not a sufficient condition to responder authentication. In fact, the execution of $r\_running(a\_id,b\_id)$can be obtained by any enemy which pretends to be B in the first message (note that if this would not be possible we would have authentication of A before the execution of the protocol, which makes no sense). So, we could have an enemy which successfully pretends to be B (action $connection(a\_id,b\_id,ok)$) and also forces B executing $r\_running(a\_id,b\_id)$, satisfying in this way the (i) condition.

Another difference is that our method is based on a NI-like property. In this way we can reuse all the research in that field. Moreover the property we check is fixed in advance, so we do not need to define a specific property for every different protocol we want to verify which is, in general, a non trivial task as we have seen above for property (i) . We can also see that the method is not tailored for authentication. In [FG], we show how to use exactly the same NI-based property and the same kind of analysis to check a simple session key distribution protocol based on public-key. In particular, in that paper we show how NI-based properties are able to detect the following two attacks:

• if the KDC (Key Distribution Center) does not sign the requested public keys, then an attacker can substitute those keys with its own key;
• if the KDC forgets to include in the signed message the identity of the owner of the key, then an attacker can fake the request from a user to KDC in such a way that the user receives the enemy key.