Formal Analysis and Design of Authentication Protocols

Formal Analysis and Design of Authentication Protocols

Siraj Ahmed Shaikh (United Nations University (UNU), Macau, SAR China)
Copyright: © 2009 |Pages: 14
DOI: 10.4018/978-1-59904-855-0.ch020
OnDemand PDF Download:


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.
Chapter Preview


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.

Complete Chapter List

Search this Book:
Editorial Advisory Board
Table of Contents
Jatinder N. D. Gupta, Sushil Sharma
Jatinder N. D. Gupta, Sushil Sharma
Chapter 1
Xin Luo, Qinyu Liao
In computer virology, advanced encryption algorithms, on the bright side, can be utilized to effectively protect valuable information assets of... Sample PDF
Ransomware: A New Cyber Hijacking Threat to Enterprises
Chapter 2
Joon S. Park
E-commerce has grown immensely with the increase in activity on the Internet, and this increase in activity, while immeasurable, has also presented... Sample PDF
E-Commerce: The Benefits, Security Risks, and Countermeasures
Chapter 3
Pamela Ajoku
Even though weapons and money are considered important factors for running a modern world, at the end of the day, it is all about controlling and... Sample PDF
Information Warfare: Survival of the Fittest
Chapter 4
Gaeil An, Joon S. Park
In this chapter, we discuss the evolution of the enterprise security federation, including why the framework should be evolved and how it has been... Sample PDF
Evolution of Enterprise Security Federation
Chapter 5
Roy Ng
The hypergrowth of computing and communications technologies increases security vulnerabilities to organizations. The lack of resources training... Sample PDF
A Holistic Approach to Information Security Assurance and Risk Management in an Enterprise
Chapter 6
John D’Arcy, Anat Hovav
A number of academic studies that focus on various aspects of information security management (ISM) have emerged in recent years. This body of work... Sample PDF
An Integrative Framework for the Study of Information Security Management Research
Chapter 7
Aditya Ponnam
Organizations worldwide recognize the importance of a comprehensive, continuously evolving risk assessment process, built around a solid risk... Sample PDF
Information Systems Risk Management: An Audit and Control Approach
Chapter 8
Udaya Kiran Tupakula
In this chapter we discuss Distributed Denial of Service (DDoS) attacks in networks such as the Internet, which have become significantly prevalent... Sample PDF
Distributed Denial of Service Attacks in Networks
Chapter 9
Andy Luse
This chapter describes various firewall conventions, and how these technologies operate when deployed on a corporate network. Terms associated with... Sample PDF
Firewalls as Continuing Solutions for Network Security
Chapter 10
Jamie Twycross
The immune system provides a rich metaphor for computer security: anomaly detection that works in nature should work for machines. However, early... Sample PDF
An Immune-Inspired Approach to Anomaly Detection
Chapter 11
Wasim A. Al-Hamdani
This chapter introduces cryptography from information security phase rather than from deep mathematical and theoretical aspects, along with... Sample PDF
Cryptography for Information Security
Chapter 12
Carlo Belletini
The chapter introduces and describes representative defense mechanisms to protect from both basic and advanced exploitation of low-level coding... Sample PDF
Memory Corruption Attacks, Defenses, and Evasions
Chapter 13
Dalila Boughaci, Brahim Oubeka, Abdelkader Aissioui, Habiba Drias, Belaïd Benhamou
This chapter presents the design and the implementation of a decentralized firewall. The latter uses autonomous agents to coordinately control the... Sample PDF
Design and Implementation of a Distributed Firewall
Chapter 14
Tom Coffey
This chapter concerns the correct and reliable design of modern security protocols. It discusses the importance of formal verification of security... Sample PDF
A Formal Verification Centred Development Process for Security Protocols
Chapter 15
Ahsan Habib
This chapter develops a distributed monitoring scheme that uses edge-to-edge measurements to identify congested links and capture the misbehaving... Sample PDF
Edge-to-Edge Network Monitoring to Detect Service Violations and DoS Attacks
Chapter 16
Doug White, Alan Rea
Hard disk wipes are a crucial component of computing security. However, more often than not, hard drives are not adequately processed before either... Sample PDF
A "One-Pass" Methodology for Sensitive Data Disk Wipes
Chapter 17
Lijun Liao
This chapter deals with the issues concerning e-mail communication security. We analyze the most popular security mechanisms and standards related... Sample PDF
Securing E-Mail Communication with XML Technology
Chapter 18
Li Yang, Raimund K. Ege, Lin Luo
This chapter describes our approach to handle security in a complex Distributed Virtual Environment (DVE). The modules of such an environment all... Sample PDF
Aspect-Oriented Analysis of Security in Distributed Virtual Environment
Chapter 19
Information Availability  (pages 230-239)
Deepak Khazanchi
This chapter describes the concept of information availability (IAV) which is considered an important element of information security. IAV is... Sample PDF
Information Availability
Chapter 20
Siraj Ahmed Shaikh
The purpose of this chapter is to introduce the reader to the research area of formal analysis of authentication protocols. It briefly introduces... Sample PDF
Formal Analysis and Design of Authentication Protocols
Chapter 21
Rajeev R. Raje, Alex Crespi, Omkar J. Tilak, Andrew M. Olson
Component-based software development offers a promising technique for creating distributed systems. It does require a framework for specifying... Sample PDF
Access Control Frameworks for a Distributed System
Chapter 22
Manish Gupta, JinKyu Lee, H. R. Rao
The Internet has emerged as the dominant medium in enabling banking transactions. Adoption of e-banking has witnessed an unprecedented increase over... Sample PDF
Implications of FFIEC Guidance on Authentication in Electronic Banking
Chapter 23
Sue Conger
Historically, companies have automated a security model that analogizes the concept of a “guardian” who monitors incoming and outgoing activities... Sample PDF
Disruptive Technology Impacts on Security
Chapter 24
Sushma Mishra
Internal auditing has become increasingly important in current business environments. In this era of the Sarbanes- Oxley Act and other similar... Sample PDF
Internal Auditing for Information Assurance
Chapter 25
William H. Friedman
This chapter is management oriented. It first proposes a general theoretical context for IT disasters within the wider class of all types of... Sample PDF
IT Continuity in the Face of Mishaps
Chapter 26
Yvette Ghormley
This chapter describes the tools that businesses can use to create a Business Continuity and Disaster Recovery Plan. Utilizing business modeling... Sample PDF
Business Continuity and Disaster Recovery Plans
Chapter 27
Yvette Ghormley
The number and severity of attacks on computer and information systems in the last two decades has steadily risen and mandates the use of security... Sample PDF
Security Policies and Procedures
Chapter 28
Arjmand Samuel
This chapter outlines the overall access control policy engineering framework in general and discusses the subject of validation of access control... Sample PDF
Enterprise Access Control Policy Engineering Framework
Chapter 29
Sushil K. Sharma, Jatinder N.D. Gupta
The purpose of the information security policy is to establish an organization-wide approach to prescribe mechanisms that help identify and prevent... Sample PDF
Information Security Policies: Precepts and Practices
Chapter 30
Paul D. Witman
This chapter provides a set of guidelines to assist information assurance and security researchers in creating, negotiating, and reviewing... Sample PDF
A Guide to Non-Disclosure Agreements for Researchers
Chapter 31
Omkar J. Tilak
Software realization of a large-scale Distributed Computing System (DCS) is achieved through the Componentbased Software Development (CBSD)... Sample PDF
Assurance for Temporal Compatibility Using Contracts
Chapter 32
Arjan Durresi
The latest estimates suggest that there are over two billion cell phone users worldwide. The massive worldwide usage has prompted technological... Sample PDF
Spatial Authentication Using Cell Phones
Chapter 33
Sushil K. Sharma, Jatinder N.D. Gupta, Ajay K. Gupta
The ability to perform E-Commerce over the Internet has become the driver of the new digital economy. As it has opened up opportunities for... Sample PDF
Plugging Security Holes in Online Environment
Chapter 34
Erik Graham, Paul John Steinbart
This chapter presents a step-by-step approach to improving the security of wireless networks. It describes the basic threats to achieving the... Sample PDF
Six Keys to Improving Wireless Security
Chapter 35
Robert W. Proctor, E. Eugene Schultz, Kim-Phuong L. Vu
Many measures that enhance information security and privacy exist. Because these measures involve humans in various ways, their effectiveness... Sample PDF
Human Factors in Information Security and Privacy
Chapter 36
Wm. Arthur Conklin
Software defects lead to security vulnerabilities, which cost businesses millions of dollars each year and threaten the security of both individuals... Sample PDF
Threat Modeling and Secure Software Engineering Process
Chapter 37
Christopher M. Botelho, Joseph A. Cazier
The threat of social engineering attacks is prevalent in today’s society. Even with the pervasiveness of mass media’s coverage of hackers and... Sample PDF
Guarding Corporate Data from Social Engineering Attacks
Chapter 38
Tom Clark
Data storage is playing an increasingly visible role in securing application data in the data center. Today virtually all large enterprises and... Sample PDF
Data Security for Storage Area Networks
Chapter 39
Edgar Weippl
This chapter outlines advanced options for security training. It builds on previous publications (Weippl 2005, 2006) and expands them by including... Sample PDF
Security Awareness: Virtual Environments and E-Learning
Chapter 40
Manish Gupta
Enterprises are increasingly interested in new and cost effective technologies to leverage existing investments in IT and extend capabilities to... Sample PDF
Security-Efficient Identity Management Using Service Provisioning (Markup Language)
Chapter 41
Dwayne Stevens, David T. Green
Voice over Internet Protocol (VoIP) networks signal an evolution in telecommunications that is accelerating the convergence of the Internet and the... Sample PDF
A Strategy for Enterprise VoIP Security
Chapter 42
Jose M. Torres
This chapter presents an Information Systems Security Management Framework (ISSMF) which encapsulates eleven Critical Success Factors (CSFs) along... Sample PDF
Critical Success Factors and Indicators to Improve Information Systems Security Management Actions
Chapter 43
Rebecca H. Rutherfoord
This chapter will deal with issues of privacy, societal, and ethical concerns in enterprise security. Security for a company is defined as... Sample PDF
Privacy, Societal, and Ethical Concerns in Security
Chapter 44
Rodolfo Villarroel, Eduardo Fernández-Medina, Juan Trujillo, Mario Piattini
This chapter presents an approach for designing secure Data Warehouses (DWs) that accomplish the conceptual modeling of secure DWs independently... Sample PDF
An MDA Compliant Approach for Designing Secure Data Warehouses
Chapter 45
Hai Wang
This chapter introduces the survivability evaluation, especially on the corresponding evaluation criteria and modeling techniques. The content of... Sample PDF
Survivability Evaluation Modeling Techniques and Measures
Chapter 46
Art Taylor
With the rise of the Internet, computer systems appear to be more vulnerable than ever from security attacks. Much attention has been focused on the... Sample PDF
The Last Line of Defense: A Comparison of Windows and Linux Authentication and Authorization Features
Chapter 47
M. Pradhan
Information Technology can be used at all levels to counter attack bioterrorism. This article gives an overview of use of Information Technology for... Sample PDF
Bioterrorism and Biosecurity
About the Contributors