Abstract
This paper is concerned with the design and verification of security protocols. It focuses on how to prevent protocol design weaknesses that are exploitable by intruder replay attacks. The reasons why protocols are vulnerable to replay attack are analysed and based on this analysis a new set of design guidelines to ensure resistance to these attacks is proposed. Further, an empirical study using a verification tool is carried out on a range of protocols that are known to be vulnerable to replay attacks, as well as some amended versions that are known to be free of these weaknesses. The goal of this study is to verify conformance of the protocols to the proposed design guidelines, by establishing that protocols which do not adhere to these guidelines contain weaknesses that are exploitable by replay attacks. Where non-conformance with the design guidelines is established by the verification tool the protocol can be amended to fix the design flaw.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Coffey, T., Dojen, R., Flanagan, T.: Formal verification: An imperative step in the design of security protocols. Computer Networks 43(5), 601–618 (2003)
Nam, J., Kim, S., Park, S., Won, D.: Security Analysis of a Nonce-Based User Authentication Scheme Using Smart Cards. IEICE Transactions Fundamentals E90-A(1), 299–302 (2007)
Fu, X., Guo, Y.: A Lightweight RFID Mutual Authentication Protocol with Ownership Transfer. In: Wang, R., Xiao, F. (eds.) CWSN 2012. CCIS, vol. 334, pp. 68–74. Springer, Heidelberg (2013)
Dojen, R., Pasca, V., Coffey, T.: Impersonation Attacks on a Mobile Security Protocol for End-to-End Communications. In: Schmidt, A.U., Lian, S. (eds.) MobiSec 2009. LNICST, vol. 17, pp. 278–287. Springer, Heidelberg (2009)
Dojen, R., Jurcut, A., Coffey, T., Györödi, C.: On Establishing and Fixing a Parallel Session Attack in a Security Protocol. In: Badica, C., Mangioni, G., Carchiolo, V., Burdescu, D.D. (eds.) Intelligent Distributed Computing, Systems and Applications. SCI, vol. 162, pp. 239–244. Springer, Heidelberg (2008)
Lowe, G.: Some new attacks upon security protocols. In: Proc. 9th IEEE Computer Security. Foundations Workshop, pp. 162–169 (1996)
Hsiang, H.C., Shih, W.K.: Weaknesses and improvements of the Yoon-Ryu-Yoo remote user authentication scheme using smart cards. Computer Communications 32, 649–652 (2009)
Wang, D., Ma, C.: Cryptanalysis of a remote user authentication scheme for mobile client-server environment based on ECC. Information Fusion 14, 498–503 (2013)
Jurcut, A., Coffey, T., Dojen, R.: Establishing and Fixing Security Protocols Weaknesses using a Logic-based Verification Tool. Journal of Communication 8(11), 795–806 (2013)
Coffey, T., Dojen, R., Jurcut, A.: CDVT/AD Verification Tool 2014 Executable, www.dcsl.ul.ie/cdvt-ad-tool
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems TOCS 8(1), 18–36 (1990)
Satyanarayanan, M.: Integrating security in a large distributed system. ACM Transactions on Computer Systems 7(3), 247–280 (1989)
Denning, D., Sacco, G.: Timestamps in key distributed protocols. Communication of the ACM 24(8), 533–535 (1981)
Clark, J., Jacob, J.: On the security of recent protocols. Information Processing Letters 56, 151–155 (1995)
Kao, I., Chow, R.: An efficient and secure authentication protocol using uncertified keys. Operating Systems Review 29(3), 14–21 (1995)
Dojen, R., Lasc, I., Coffey, T.: Establishing and Fixing a Freshness Flaw in a Key-Distribution and Authentication Protocol. In: IEEE International Conference on Intelligent Computer Communication and Processing, pp. 185–192 (2008)
Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. Software Engineering 23(10), 659–669 (1997)
Xu, S., Huang, C.: Attacks on PKM Protocols of IEEE 802.16 and Its Later Versions. In: Proceedings of 3th International Symposium on Wireless Communication System (ISWCS), pp. 185–189. IEEE Press, Spain (2006)
Dojen, R., Zhang, F., Coffey, T.: On the Formal Verification of a Cluster Based Key Management Protocol for Wireless Sensor Networks. In: International Performance Computing and Communications Conference, Texas, USA, pp. 499–506 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Jurcut, A.D., Coffey, T., Dojen, R. (2014). On the Prevention and Detection of Replay Attacks Using a Logic-Based Verification Tool. In: Kwiecień, A., Gaj, P., Stera, P. (eds) Computer Networks. CN 2014. Communications in Computer and Information Science, vol 431. Springer, Cham. https://doi.org/10.1007/978-3-319-07941-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-07941-7_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07940-0
Online ISBN: 978-3-319-07941-7
eBook Packages: Computer ScienceComputer Science (R0)