Abstract
This chapter concerns the correct and reliable design of modern security protocols. It discusses the importance of formal verification of security protocols prior to their release by publication or implementation. A discussion on logic-based verification of security protocols and its automation provides the reader with an overview of the current state-of-the-art of formal verification of security protocols. The authors propose a formal verification centred development process for security protocols. This process provides strong confidence in the correctness and reliability of the designed protocols. Thus, the usage of weak security protocols in communication systems is prevented. A case-study on the development of a security protocol demonstrates the advantages of the proposed approach. The case-study concludes with remarks on the performance of automated logic-based verification and presents an overview of formal verification results of a range of modern security protocols.
TopIntroduction
The security of electronic networks and information systems is a critical issue for the use of new technologies in all fields of life. Mobile and fixed networks are trusted with highly sensitive information. Thus, security protocols (also called cryptographic protocols) are required to ensure the security of both the infrastructure itself and the information that runs through it. These security protocols can be thought of as the keystones of a secure architecture. Basic cryptographic protocols allow agents to authenticate each other, to establish fresh session keys for confidential communication and to ensure the authenticity of data and services. Building on such basic cryptographic protocols, more advanced services like nonrepudiation, fairness, electronic payment, and electronic contract signing are achieved.
The massive growth in communications technologies—in particular in the wireless sector—causes an ever-changing environment for today’s communication services. The pervasive nature of emerging Information and Communications Technologies has added new areas of concern to information security. For example, the increased virtual and physical mobility of users enhances their possibilities for interaction, but leads to an increasing demand for reliable trust relationships. To address new security risks and threats arising from such changes in the communication environment, a constant supply of novel security protocols is required.
However, security protocols are vulnerable to a host of subtle attacks, and designing protocols to be impervious to such attacks has been proven to be extremely challenging and error-prone. This is evident from the surprisingly large number of published protocols, which have later been found to contain various flaws, in many cases, several years after the original publication (Brackin, 2000; Coffey, Dojen, & Flangan, 2003a, 2003b, 2003c, 2003d; Huima, 1999; Gürgens & Rudolph, 2002; Newe & Coffey, 2002; Ventuneac, Coffey, & Newe, 2004; Ventuneac, Dojen, & Coffey, 2006; Zhang & Fang, 2005; Zhang & Varadharajan, 2001).
Key Terms in this Chapter
Authentication: The verification of the identity of the source of information.
Formal Verification: Application of formal methods to establish the correctness of a system.
Data Integrity: The provision of the property that data and data sequences have not been altered or destroyed in an unauthorized manner.
Cryptography: The study of mathematical techniques related to aspects of information security such as confidentiality, data integrity, entity authentication, and data origin authentication.
Nonrepudiation: Nonrepudiation is the concept of ensuring that a contract, especially one agreed to via the Internet, cannot later be denied by one of the parties involved. With regards to digital security, nonrepudiation means that it can be verified that the sender and the recipient were, in fact, the parties who claimed to send or receive the message, respectively.
Security Protocol: Also called cryptographic protocol, it constitutes transferring specially constructed encrypted messages between legitimate protocol participants to fulfil objectives such as mutual authentication or key-exchange in a predefined procedure.
Confidentiality: The protection of information, so that someone not authorized to access the information cannot read the information, even though the unauthorized person might see the information’s container.
Formalisation of a Security Protocol: Specifying the protocol in the language of the logic by expressing each protocol message as a logical formula is known as protocol formalisation (or idealisation). A formal description of the protocol, obtained by formalisation, does not simply list the components of each message, but attempts to show the purpose of these components so as to avoid ambiguity.
Postulate: A proposition that is accepted as true in order to provide a basis for logical reasoning.
Nonce: A large random number that is intended to be employed only once and is used for binding messages to a specific protocol run.