Elsevier

Computers & Security

Volume 45, September 2014, Pages 255-273
Computers & Security

Design guidelines for security protocols to prevent replay & parallel session attacks

https://doi.org/10.1016/j.cose.2014.05.010Get rights and content

Abstract

This work is concerned with the design of security protocols. These protocols are susceptible to intruder attacks and their security compromised if weaknesses in the protocols' design are evident. In this paper a new analysis is presented on the reasons why security protocols are vulnerable to replay and parallel session attack and based on this analysis a new set of design guidelines to ensure resistance to these attacks is proposed. The guidelines are general purpose so as to encompass a wide spectrum of security protocols.

Further, an empirical study on the effectiveness of the proposed guidelines is carried out on a set of protocols, incorporating those that are known to be vulnerable to replay or parallel session attacks as well as some amended versions that are known to be free of these weaknesses. The goal of this study is to establish conformance of the set of protocols with the proposed design guidelines. The results of the study show that any protocol following the design guidelines can be considered free of weaknesses exploitable by replay or parallel session attacks. On the other hand, if non-conformance of a protocol with the design guidelines is determined, then the protocol is vulnerable to replay or parallel session attacks.

Introduction

Cryptographic protocols play an important role in today's communications environment, where they are used to provide a wide variety of security services, such as: key distribution, data confidentiality, authentication and non-repudiation.

The design of provably secure protocols is complex and prone to error, where the main difficulty is to address the vast possibilities of an adversary to gain information (Dojen and Coffey, 2005). These protocols can be vulnerable to a host of subtle attacks that compromise the services they provide; so designing them to be impervious to such attacks has proved to be extremely challenging. Many published security protocols have subsequently been found to contain security weaknesses that are exploitable by attacks. The public key authentication of Needham and Schroeder (Needham and Schroeder, 1978), for example, was considered secure for over a decade. Other protocol weaknesses exploitable by attacks can be found in: (Denning and Sacco, 1981, Burrows et al., 1990, Syverson, June 1994, Lowe, 1996, Abadi, March 1997, Heather et al., 2000). The difficulty of designing security protocols that are free of mountable attacks continues today, as highlighted by many recently found instances of replay and parallel session attacks:

  • attacks found in 2003 (Coffey et al., December 2003) on several authentication and key agreement protocols for mobile communications (Beller et al., 1993, Carlsen, 1994, Mu and Varadharajan, 1996)

  • attacks found in 2006 (Xu & Huang, September, 2006) and 2008 (Altaf et al., 2008) on privacy and key management IEEE Std. 802.16e-2005 protocol, (IEEE Std. 802.16e/D12, 2005)

  • attacks (Nam et al., Jan 2007) found in 2007 on an authentication protocol introduced in 2005 (Lee et al., 2005)

  • attack found in 2008 (Espelid et al., 2008) on Norway national security for e-commerce protocol BankID introduced in 2006 (The Norwegian Banks' Payment and Clearing Centre, 2006)

  • attack found in 2008 (Xu et al., July, 2008) on a fingerprint-based authentication scheme with smart cards introduced in 2006 (Khan and Zhang, 2006)

  • attacks found in 2008 (Dojen et al., 2008b) on a Key Management Protocol for Wireless Sensor Networks (Shen et al., 2008)

  • attack found in 2008 (Dojen et al., 2008c)on a key distribution protocol (Lowe, 1997)

  • attack found in 2009 (Hsiang and Shih, 2009) on a remote user authentication scheme using smart cards introduced in 2005 (Yoon and Yoo, 2005)

  • attacks found in 2009 (Dojen et al., 2009) on an end-to-end authentication and secrecy protocol introduced in 2003 (Lee et al., 2003)

  • attacks found in 2012 (Yoo et al., 2012) on an authentication scheme introduced in 2009 (Das, 2009) and its derivatives (Nyang and Lee, 2009, Huang et al., October 2010, Chen and Shih, 2010, Khan and Alghathbar, 2010)

  • attacks found in 2013 (Wang and Ma, 2013) on ID-based scheme for mobile client–server environment introduced in 2012 (He et al., 2012)

  • attacks found in 2013 (Fu and Guo, 2013) on lightweight RFID mutual authentication protocol introduced in 2011 (Jin et al., 2011)

  • attack found in 2013 (Zhuang et al., July 2013) on RAPP ultra-lightweight RFID protocol introduced in 2012 (Tian et al., 2012)

The research work presented in this paper is concerned with the design of security protocols, in particular the prevention of design weaknesses that may be subsequently exploited by replay or parallel session attacks.

A new analysis on the reasons why freshness and parallel session attacks against security protocols succeed is presented. This analysis discovers the vulnerabilities in the structure of the protocol message exchanges that can be exploited by these attacks. Specifically, the analysis seeks answers to the questions:

  • Why are freshness and parallel session attacks successful?

  • Can the reasons be represented by a finite set of data patterns representing the message exchanges?

  • Is it possible to develop a finite set of protocol design rules or guidelines that will prevent the effectiveness of these attacks?

A new comprehensive set of guidelines for security protocols to prevent design weaknesses that are exploitable by replay or parallel session attacks is proposed. The guidelines are general purpose so as to encompass a wide spectrum of security protocols. The effectiveness of the guidelines is also established in a presented case study which shows that: (i) protocols with known weaknesses violate some of the guidelines, (ii) protocols without weaknesses do not violate any guidelines.

These guidelines are intended to be used at the design stage of security protocols. Any protocol following these guidelines can be considered to be free of any weaknesses exploitable by replay or parallel session attacks. On the other hand, if non-conformance of a protocol with the design guidelines is established, then the protocol is vulnerable to replay or parallel session attacks.

The remainder of this paper has the following structure. Section 2 gives an overview of related work and Section 3 outlines the analysed methodology used in this work. Section 4 introduces the language and definitions used through the paper. Each defined weakness type is then separately analysed and corresponding design guidelines are proposed: Section 5 addresses the issue of freshness of messages, Section 6 addresses the issue of symmetry of messages, Section 7 addresses the issue of signed messages and Section 8 addresses the issue of challenge-response handshake construction. In Section 9, the effectiveness of the proposed guidelines is evaluated by way of an empirical study on a set of protocols with known weaknesses and those that are known to be secure. The conformance of one protocol (and its amended version) is analysed in detail and the conformance of a range of protocols is presented in summary form. Finally, Section 10 concludes the paper. A summary of the proposed design guidelines is included in Appendix A.

Section snippets

Related work

The design of reliable and trustworthy security protocols has been addressed by a series of publications over the past two decades. Bird et al. (Bird et al., 1992) introduced in 1992 a two-way authentication protocol using symmetric key cryptography and gave a set of considerations to avoid weaknesses in the design of these types of protocols. This work was extended in 1993 (Bird et al., June 1993) in the form of a methodology to systematically build a family of cryptographic two-way

Analysis methodology

The goal of this analysis is to establish why replay and parallel session attacks succeed on a broad spectrum of security protocols, to propose a set of protocol design guidelines to counter these attacks and to establish the effectiveness of the proposed guidelines.

Language and definitions

This section introduces the language, considerations, definitions and predicates used through this paper. The following notation is used to classify the variables and constants of the language:

  • P: protocol

  • w, x, y, z: data objects (atomic or composite)

  • A, B, C: legitimate principals

  • TTP: trusted third party principal

  • I(A)/I(B): intruder masquerading as principal A/B

  • ENT(P): set of all principals involved in a protocol P

  • x : data component generated by principal A

  • k: any cryptographic key, where

Analysing problems related to freshness of messages

Consider two principals A and B involved in a protocol P (A,BENT(P)). In an arbitrary step Sr of the protocol P, A sends a message containing a cryptographic expression {x}k to B (∃SrP,Sr:A → B:{x}k). If this cryptographic expression does not have at least one component fresh for recipient B (¬∃y|C({x}k,y,Sr)∧Fresh(y,B)) then the message containing {x}k can be replayed. An intruder (I) can mislead the recipient (B) to accept old and possibly compromised data as a component of the

Analysing problems related to symmetry of messages

Consider two cryptographic transformations c1 and c2 that are exchanged directly or indirectly (↑↓(c1,c2)) between two principals A,BENT(P). If c1 and c2 are symmetric (Symmetric(c1,c2)) and principal value type equivalent messages (Pvte(c1,c2)), then expression c2 can be used instead of expression c1 or c1 can be reconstructed based on expression c2 in a parallel protocol run. In the following cases symmetry-based attacks can be mounted:

Case 1

Expressions c1 and c2 are exchanged directly in steps Sq

Analysing problems related to signed messages

Consider a protocol P, where in step Sr a signed statement {x}KAPriv is transmitted. If this signed statement is not receiver bound (¬RBound(B,{x}KAPriv)) and does not include appropriate identities of principals, then an intruder can use the signed statement {x}KAPriv in a parallel run to impersonate a legitimate principal. In the following cases signed message-based attacks can be mounted:

Case 1

{x}KAPriv is a parent cryptographic expression:

Assume ∃SrP such that A = s(Sr) and B = r(Sr). If {x}K

Analysing problems related to challenge-response handshakes construction

This section discusses issues related to challenge-response handshakes in security protocols. To facilitate the presented analysis a new classification for challenge-response handshakes and the criteria upon which they are based is introduced.

Evaluation of proposed guidelines

This study seeks to evaluate the effectiveness of the proposed design guideline by evaluating whether security protocols observe the guidelines. This evaluation considers a wide range of protocols, incorporating those with known weaknesses and their published amended versions. The guidelines are considered effective if:

  • -

    Protocols with known weaknesses violate some of the guidelines.

  • -

    Protocols without weaknesses do not violate any guidelines.

In the remainder of this study the conformance of

Conclusion

This research work investigated why replay and parallel session attacks can be successfully deployed against security protocols thus compromising their security. The analysis discovered the vulnerabilities in the structure of the protocol message exchanges that can be exploited by these attacks and also characterised the general circumstances under which these attacks can be mounted. Based on this analysis a new set of design guidelines that ensure resistance to replay and parallel session

Acknowledgement

This work was funded by Science Foundation Ireland – Research Frontiers Programme (11/RFP.1/CMS 3340).

Anca D. Jurcut received title of Bachelor of Mathematics and Computer Science from West University of Timisoara, Romania (2007) and PhD from University of Limerick, Ireland (2013). She is currently working as a postdoctoral researcher in the Department of Electronic and Computer Engineering at the University of Limerick, Ireland. Her research interests are: Cryptographic Protocols Analysis, Formal Verification of Cryptographic Protocols, Logics Based Verification Tehniques, Data Security and

References (75)

  • R.R. Ahirwal et al.

    An efficient and secure ID-based remote user authentication scheme using smart card

    International Journal of Applied Information Systems (IJAIS)

    (February 2012)
  • A. Altaf et al.

    Security Enhancements for Privacy and Key Management Protocol in IEEE 802.16e-2005

    (2008)
  • R. Anderson et al.

    Robustness principles for public key protocols

  • T. Aura

    Strategies against replay attacks

  • M.J. Beller et al.

    Privacy and authentication on a portable communications system

    IEEE Journal on Selected Areas in Communications

    (1993)
  • R. Bird et al.

    Systematic design of two-party authentication protocols

  • R. Bird et al.

    Systematic design of a family of attack-resistant authentication protocols

    IEEE Journal on Selected Areas in Communications

    (June 1993)
  • M. Burrows et al.

    A logic of authentication

    ACM Transactions on Computer Systems TOCS

    (1990)
  • U. Carlsen

    Optimal Privacy and Authentication on a portable communications system

    ACM Operating System Reviews

    (1994)
  • U. Carlsen

    Cryptographic protocol flaws

  • CCITT

    The directory authentification framework

    (1987)
  • T.H. Chen et al.

    A robust mutual authentication protocol for wireless sensor networks

    ETRI Journal

    (2010)
  • J. Clark et al.

    A survey of authentication protocol literature: Version 1.0

    (November 1997)
  • M.L. Das

    Two-factor user authentication in wireless sensor networks

    IEEE Trans on Wireless Communications

    (2009)
  • D. Denning et al.

    Timestamps in key distributed protocols

    Communications of the ACM

    (1981)
  • R. Dojen et al.

    Layered proving trees: a novel approach to the automation of logic-based security protocol verification

    ACM Transactions on Information Systems Security (TISSEC)

    (2005)
  • R. Dojen et al.

    Establishing and fixing a freshness flaw in a key-distribution and authentication protocol

    (August 2008)
  • R. Dojen et al.

    Impersonation attacks on a Mobile security protocol for end-to-end communications

  • R. Dojen et al.

    On the formal verification of a cluster based key management protocol for wireless sensor networks

    (2008)
  • R. Dojen et al.

    On establishing and fixing a parallel session attack in a security protocol

    (2008)
  • Y. Espelid et al.

    A proof of concept attack against Norwegian internet banking systems

  • X. Fu et al.

    A lightweight RFID mutual authentication protocol with ownership transfer

    (2013)
  • L. Gong et al.

    Fail-stop protocols: an approach to designing secure protocols

  • A. Gordon et al.

    Types and effects for asymmetric cryptographic protocols

    Journal of Computer Security

    (2004)
  • D. He et al.

    An id-based client authentication with key agreement protocol for mobile client–server environment on ECC with provable security

    Information Fusion

    (2012)
  • J. Heather et al.

    How to prevent type flaw attacks on security protocols

    (2000)
  • H.F. Huang et al.

    Enhancement of two-factor user authentication in wireless sensor networks

  • Cited by (0)

    Anca D. Jurcut received title of Bachelor of Mathematics and Computer Science from West University of Timisoara, Romania (2007) and PhD from University of Limerick, Ireland (2013). She is currently working as a postdoctoral researcher in the Department of Electronic and Computer Engineering at the University of Limerick, Ireland. Her research interests are: Cryptographic Protocols Analysis, Formal Verification of Cryptographic Protocols, Logics Based Verification Tehniques, Data Security and Network Security, Software Engineering, Engineering Mathematics.

    Tom Coffey is Professor of Electronic and Computer Engineering at the University of Limerick, Ireland, where he is also director and founder of Data Communication Security Laboratory. He is a Chartered Engineer; he holds Master of Science (1978) and Doctor of Philosophy (1994) degrees from City University (London) and University of Ulster (Ireland) respectively. His research work encompasses: encryption systems, verifiably secure cryptographic protocols for open hostile environments, formal verification of security protocols using logic-based and state space-based techniques, generation of modal-logics of knowledge and belief, automated proving systems for security protocol verification.

    Reiner Dojen is currently employed as Lecturer in the Department of Electronic and Computer Engineering at the University of Limerick, Ireland. Received title of Diplom-Ingenieur (FH) (1999) from University of Applied Sciences Osnabrück, Germany, Master of Engineering (2000) from University of Limerick and Doctor of Philosophy (2004) from University of Limerick. His research interests include design and verification of security protocols, design and implementations of verification techniques for security protocols, data and network Security, automated theorem proving and artificial intelligence.

    View full text