Journal of Computer Security

Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However, there is a huge gulf between these and most large commercial protocols: the latter typically have many more fields, and much higher levels of nested encryption. As a result, existing techniques are difficult to apply directly to these large protocols.

In this paper we develop the notion of fault-preserving simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of such fault-preserving simplifying transformations, and use them in the analysis of a commercial protocol.

We propose a new efficient automatic verification technique, Athena, for security protocol analysis. It uses a new efficient representation – our extension to the Strand Space Model, and utilizes techniques from both model checking and theorem proving approaches. Athena is fully automatic and is able to prove the correctness of many security protocols with arbitrary number of concurrent runs. The run time for a typical protocol from the literature, like the Needham–Schroeder protocol, is often a fraction of a second.

Athena exploits several different techniques that enable it to analyze infinite sets of protocol runs and achieve such efficiency. Our extended Strand Space Model is a natural and efficient representation for the problem domain. The security properties are specified in a simple logic which permits both efficient proof search algorithms and has enough expressive power to specify interesting properties. The automatic proof search procedure borrows some efficient techniques from both model checking and theorem proving. We believe that it is the right combination of the new compact representation and all the techniques that actually makes Athena successful in fast and automatic verification of security protocols.

Various formulations of non-interference have been proposed to try to characterise the absence of information flows in system or network. There is still no consensus in the information security community as to which of these accurately captures our intuition of the notion of secrecy.

We argue that non-interference is closely related to the characterisation of process equivalence. What constitutes process equivalence is itself a fundamental question in computer science with several distinct definitions proposed in the literature. We illustrate how several of the definitions of non-interference mirror notions of process equivalence. Casting these security concepts in a process algebraic framework clarifies, for example, the role of non-determinism and allows results to be carried over regarding composition and the completeness of unwinding rules. We also discuss some natural generalisations of the approach.

Abadi has introduced a logic to explicate the meaning of local names in SDSI, the Simple Distributed Security Infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however; it draws conclusions about local names that do not follow from SDSI's name resolution algorithm. Moreover, its semantics is somewhat unintuitive. This paper presents the Logic of Local Name Containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.

Denial of service is becoming a growing concern. As computer systems communicate more and more with others that they know less and less, they become increasingly vulnerable to hostile intruders who may take advantage of the very protocols intended for the establishment and authentication of communication to tie up resources and disable servers. This paper shows how some principles that have already been used to make cryptographic protocols more resistant to denial of service by trading off the cost to defender against the cost to the attacker can be formalized based on a modification of the Gong–Syverson fail-stop model of cryptographic protocols, and indicates the ways in which existing cryptographic protocol analysis tools could be modified to operate within this formal framework. We also indicate how this framework could be extended to protocols that do not make use of strong authentication.