Design guidelines for security protocols to prevent replay & 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,B∈ENT(P)). In an arbitrary step Sr of the protocol P, A sends a message containing a cryptographic expression {x}k to B (∃Sr∈P,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,B∈ENT(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 ∃Sr∈P 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)
- et al.
On the security of recent protocols
Information Processing Letters
(1995) - et al.
Formal verification: an Imperative step in the design of security protocols
Comput Networks Journal
(December 2003) - et al.
Weaknesses and improvements of the Yoon-Ryu-Yoo remote user authentication scheme using smart cards
Computer Communications
(2009) - et al.
On the security of splice/as : the authentication system in wide internet
Information Processing Letters
(1995) - et al.
Two attacks on neumann-stubblebine authentication protocols
Information Processing Letters
(1995) - et al.
On the detection of desynchronisation attacks against security protocols that use dynamic shared secrets
Computers & Security
(2013) - et al.
Efficient nonce-based remote user authentication scheme using smart cards
Applied Mathematics and Computation
(2005) - et al.
Cryptanalysis of a remote user authentication scheme for mobile client–server environment based on ECC
Information Fusion
(2013) - et al.
Prudent engineering practice for cryptographic protocols
IEEE Transactions on Software Engineering
(1996) Explicit communication Revisited: two new attacks on authentication protocols
IEEE Transactions on Software Engineering
(March 1997)
An efficient and secure ID-based remote user authentication scheme using smart card
International Journal of Applied Information Systems (IJAIS)
Security Enhancements for Privacy and Key Management Protocol in IEEE 802.16e-2005
Robustness principles for public key protocols
Strategies against replay attacks
Privacy and authentication on a portable communications system
IEEE Journal on Selected Areas in Communications
Systematic design of two-party authentication protocols
Systematic design of a family of attack-resistant authentication protocols
IEEE Journal on Selected Areas in Communications
A logic of authentication
ACM Transactions on Computer Systems TOCS
Optimal Privacy and Authentication on a portable communications system
ACM Operating System Reviews
Cryptographic protocol flaws
The directory authentification framework
A robust mutual authentication protocol for wireless sensor networks
ETRI Journal
A survey of authentication protocol literature: Version 1.0
Two-factor user authentication in wireless sensor networks
IEEE Trans on Wireless Communications
Timestamps in key distributed protocols
Communications of the ACM
Layered proving trees: a novel approach to the automation of logic-based security protocol verification
ACM Transactions on Information Systems Security (TISSEC)
Establishing and fixing a freshness flaw in a key-distribution and authentication protocol
Impersonation attacks on a Mobile security protocol for end-to-end communications
On the formal verification of a cluster based key management protocol for wireless sensor networks
On establishing and fixing a parallel session attack in a security protocol
A proof of concept attack against Norwegian internet banking systems
A lightweight RFID mutual authentication protocol with ownership transfer
Fail-stop protocols: an approach to designing secure protocols
Types and effects for asymmetric cryptographic protocols
Journal of Computer Security
An id-based client authentication with key agreement protocol for mobile client–server environment on ECC with provable security
Information Fusion
How to prevent type flaw attacks on security protocols
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.