Abstract
As the number of security-critical, online applications grows, the protection of the digital identities of the users is becoming a growing concern. Strong authentication protocols provide additional security by requiring the user to provide at least two independent proofs of identity for the authentication to succeed. In this paper we provide a formal model and mechanical security analysis of two protocols for two-factor and two-channel authentication for web applications that relies on the user’s mobile phone as a second authentication factor and the GSM/3G communication infrastructure as the second communication channel. By using a model checker we detected vulnerabilities in the protocols that allow an attacker to carry out a security-sensitive operation by using only one of the two authentication factors. We also present a fix that allows to patch the protocols.
This work has partially been supported by the FP7-ICT Project SPaCIoS (no. 257876) and by the project SIAM in the context of the FP7 EU “Team 2009 - Incoming” COFUND action. We would like to thank Alessio Lepre and Gianluca Buelloni of AliasLab for their helpful comments on the paper.
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
AliasLab. SecureCall Authorization - Web Services Interface v3.0. Technical report, AliasLab (February 2010)
Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: JANCL, Special Issue on Logic and Information Security. Hermes Lavoisier (2009)
Armando, A., Carbone, R., Zanetti, L.: Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols (2013), http://www.ai-lab.it/armando/pub/nss13-extended.pdf
Chou, D., Microsoft Corporation: Strong user authentication on the web, http://msdn.microsoft.com/en-us/library/cc838351.aspx (accessed September 20, 2012)
DeFigueiredo, D.: The Case for Mobile Two-Factor Authentication. S&P (2011)
Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29) (1983)
Hagalisletto, A.M.: Analyzing two-factor authentication devices. T.r., U. of Oslo (2007)
Hagalisletto, A.M.: Attacks are protocols too. In: ARES, pp. 1197–1206 (2007)
Lowe, G.: A hierarchy of authentication specifications. In: Proc. CSFW. IEEE (1997)
RSA. Enhancing one-time passwords for protection against real-time phishing attacks, www.rsasecurity.com (accessed September 20, 2012)
van Thanh, D., Jorstad, I., Jonvik, T., van Thuan, D.: Strong authentication with mobile phone as security token. In: MASS 2009, pp. 777–782 (October 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Carbone, R., Zanetti, L. (2013). Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols. In: Lopez, J., Huang, X., Sandhu, R. (eds) Network and System Security. NSS 2013. Lecture Notes in Computer Science, vol 7873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38631-2_63
Download citation
DOI: https://doi.org/10.1007/978-3-642-38631-2_63
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38630-5
Online ISBN: 978-3-642-38631-2
eBook Packages: Computer ScienceComputer Science (R0)