NI is indeed an alternative, more general approach to computer security. It requires to control directly the whole flow of information, rather than the accesses of subjects to objects (as in classical access control rules). In general, NI-like properties are based on a formal model of system behaviour and on a definition of information flow on such a model. By imposing some information flow rules, we can control both the direct and indirect transmission channels.
Although the basic motivation for NI properties was the analysis of information flows inside systems, the basic ideas behind them are very general and potentially applicable to other related security areas. The aim of this paper is precisely to show that the theory of NI properties can be profitably applied in typical problems of network security. As a simple case study, we consider the paradigmatic example of the Needham-Schroeder public-key protocol, that was already shown incorrect and fixed in [Low96]. As expected, our analysis discovers the same bug; what is really new is the methodology, based on the idea of proving the absence of information flow between the protocol partners and potential external attackers. This methodology is general and is not tailored for authentication protocols. In [FG] the same technique presented here is used to check a simple session key distribution protocol based on public-key (see Section 7 for more details on this issue).
The basic idea which permits to express authentication requirements using NI-based properties is very simple: we want to check if an enemy is able to interfere with the correct execution of the protocol; so, what we do is to check if the actions executed by the enemy interfere with the actions which characterize the successful authentication. As an example, in the attack reported in [Low96] we have that B is convinced to communicate with A but A has never sent an authentication request to B . This anomalous behaviour is caused by the enemy, which is thus able to interfere on two particular actions which we introduce to model the protocol behaviour: the first represents the authentication request from A to B (identified by the first message of the protocol) and the second represents the successful completion of the protocol by B (identified by the second message of the protocol). This enemy interference on the protocol can be detected by NI-based properties.
The method is general, since we do not give a definition of authentication. We simply need to select particular events that we want to observe and which represent the correct execution of the protocol. One typical choice is: one action representing the start of the protocol and two actions representing the correct termination of the protocol for the two partners.
The formal verification of these properties is fully automatized thanks to the CoSeC tool [FG,FG96] that accepts finite-state protocol specifications and check over them the NI-based information flow properties.
The paper is organized as follows. In Section 2 we present the model and the NI-based properties we use in the protocol specification and analysis. In Section 3 we recall the Needham-Schroeder public-key protocol and in Section 4 we specify it using our language. Section 5 is about the attacker specification. In Section 6 we analyze the protocol using NI-based properties. Finally, Section 7 is devoted to the comparison with related work.