Abstract
The purpose of this chapter is to introduce the reader to the research area of formal analysis of authentication protocols. It briefly introduces the basic notions of cryptography and its use in authentication protocols. The chapter looks at the Needham-Schroeder (1978) protocol as an example of an authentication protocol, and examines the history of the protocol as a stimulus to the formal analysis of such protocols. We then introduce the process algebra CSP (Hoare, 1985) to model authentication protocols and present Schneider’s (1998) rank function approach to analysing such protocols. The chapter concludes by describing related ongoing work in this area of research and highlight some of the challenges posed by the problem of analysing and designing protocols.
TopIntroduction
Modern communications technology allows us to communicate faster than ever before, with much higher capacity for more diverse types of data. Along with its wider reach in society, in the form of both mobility and relatively affordable access, modern communications has transformed the world we live in—serving as bedrock for electronic commerce and, other digital and communication services. The Internet has become an integral part of the personal, professional, and economic spheres of our daily life. Global organisations, whether official, commercial, or social, are relying on the Internet ever more to function, bringing an increasing need for a secure and trusted electronic infrastructure.
The pervasive nature of the Internet, one major factor behind its success, is also proving to be its main threat. Once connected to this global network, no one is more than a few clicks away from Web servers hosting web sites transacting commerce worth millions or critical state-run infrastructures running sensitive operations. Such Internet systems are threatened by both hackers with malicious and fraudulent intent, and software technology designed using indefinite and imprecise methods.
Security protocols, being developed for more than two decades now, aim to protect and secure networked systems from such threats. Using mathematically-sound yet simple cryptographic methods, these protocols are designed to provide a range of communication security services, such as authentication, confidentiality, and nonrepudiation. These protocols allow networked entities to engage with each other and derive guarantees about each other’s identity, state of knowledge and participation. An early example of such a protocol is due to Needham and Schroeder (1978), who introduced a two-party protocol to authenticate both participants to each other. The Needham-Schroeder protocol, as it has since come to be known, was a forerunner of the many security protocols that were to follow. While interest in formal design and analysis of security protocols has greatly increased, Needham and Schroeder (1978) made the first suggestion towards such an effort in the seminal presentation of their protocol:
...protocols such as those developed here are prone to extremely subtle errors that are unlikely to be detected in normal operation. The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area...
Burrows, Abadi, and Needham (1990) were the first to contribute a formal method to analyse the security goals—particularly the authentication goals—of such protocols as a system of belief logic. Interestingly, the original Needham-Schroeder protocol was formally verified to be correct using the logic.
Significant impetus for such formal analysis and verification, however, was provided much later when “subtle errors” were identified in this very protocol by Needham and Schroeder, as a result of an attack by Lowe (1995). The discovery of such an attack brought to light the difficulty over not only the design of such protocols, but also their formal analysis, stimulating a tremendous research interest. Of the many formalisms introduced to analyse and verify the design of security protocols, Lowe’s (1996) model-checking approach using the process algebra Communicating Sequential Processes (CSP) (Hoare, 1985), Meadow’s (1996) specialist tool—known as the NRL Protocol Analyzer—Gordon and Jeffrey’s (2001) type-checking approach, and Thayer, Herzog, and Guttman’s (1998)strand spaces are noteworthy.
Key Terms in this Chapter
Intruder: The term intruder is used to refer to an entity that interacts with or takes part in a protocol with intent to undermine the goals of the protocol. Also known as an enemy, attacker, spy, eavesdropper, penetrator, opponent, or an insider.
Communicating Sequential Processes (CSP): A formal language for describing patterns of interaction for concurrent systems (in computer science). First described by Sir Professor Tony Hoare at Oxford in 1978, it is a member of the family of mathematical theories of concurrency known as process algebras. It is traditionally written in a fairly mathematical notation with special symbols representing its operators, and is typeset more like mathematics than a typical programming language.
Protocol: A set of guidelines for governing communication between two or more electronic entities. Protocol are usually characterised by communication or security goals they are designed to provide (such as reliability, confidentiality, or authentication), the communication medium they are designed to operate on (such as wired or wireless), or some specific functionality (such as tunnelling).
Authentication: Authentication is a security goal and refers to the verification of a real or digital identity of a person, an electronic node, or device. In the context of protocols, this refers to the verification of a message sender’s or protocol participant’s identity.
Rank Function: A rank function is a function from a set of messages (or a message space) to the set of integers. The purpose of this function is to partition the messages, so as to characterise those messages that an intruder may get hold and those that an intruder may not get hold of. In the context of protocol analysis, this is helpful in analysing those messages that are critical to the correctness of the protocol, but are leaked to the intruder during execution.
Attack: An attack refers to the violation of the security goal of a system or a protocol. The term is commonly used to describe intentional (as opposed to accidental) violations, and involves an intruder actively (or passively) manipulating protocol messages and interactions with other participants.
Nonce: Also known as a cryptographic nonce, it refers to a random or pseudorandom number particularly used to ensure the freshness (or recentness) of some message or communication in protocols.