Abstract
Küsters and Truderung recently proposed an automatic verification method for security protocols with exclusive or (XOR). Their method reduces protocols with XOR to their XOR-free equivalents, enabling efficient verification by tools such as ProVerif. Although the proposed method works efficiently for verifying secrecy, verification of authentication properties is inefficient and sometimes impossible.
In this paper, we improve the work by Küsters and Truderung in two ways. First, we extend their method for authentication verification to a richer class of XOR-protocols by automatically introducing bounded verification. Second, we improve the efficiency of their approach by developing a number of dedicated optimizations. We show the applicability of our work by implementing a prototype and applying it to both existing benchmarks and RFID protocols. The experiments show promising results and uncover a flaw in a recently proposed RFID protocol.
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
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, Springer, Heidelberg (1996)
Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE Computer Society, Los Alamitos (2001)
Cremers, C., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic protocol analysis. In: Formal to Practical Security. LNCS, vol. 5458, pp. 70–94. Springer, Heidelberg (2009)
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. 8th Annual IEEE Symposium on Logic in Computer Science, pp. 271–280. IEEE Computer Society Press, Los Alamitos (2003)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the security of XOR-based key management schemes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 538–552. Springer, Heidelberg (2007)
Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Proc. 10th Computer Security Foundations Workshop, pp. 18–30. IEEE Computer Society Press, Los Alamitos (1997)
Küsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. In: Proc. 15th ACM Conference on Computer and Communications Security, pp. 129–138. ACM Press, New York (2008)
Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming 50(1-3), 51–71 (2004)
Chen, X., van Deursen, T., Pang, J.: Improving automatic verification of protocols with XOR (implementation) (2009), http://satoss.uni.lu/software/
International Business Machines Corporation: CCA basic services reference and guide (2003), http://www-306.ibm.com/security/cryptocards/pdfs/CCA_Basic_Services_241_Revised_20030918.pdf
Millen, J.K.: A necessarily parallel attack. In: Proc. Workshop on Formal Methods and Security Protocols (1999)
Lee, S., Asano, T., Kim, K.: RFID mutual authentication scheme based on synchronized secret information. In: Proc. Symposium on Cryptography and Information Security (2006)
Song, B., Mitchell, C.J.: RFID authentication protocol for low-cost tags. In: Proc. 2nd ACM Conference on Wireless Network Security, pp. 140–147. ACM Press, New York (2008)
van Deursen, T., Radomirović, S.: Algebraic attacks on RFID protocols. In: Jaap-Henk, H. (ed.) WISTP 2009. LNCS, vol. 5746, pp. 38–51. Springer, Heidelberg (2009)
Choi, E.Y., Lee, D.H., Lim, J.I.: Anti-cloning protocol suitable to EPCglobal class-1 generation-2 RFID systems. Computer Standards & Interfaces (in press, 2009)
Cai, Q., Zhan, Y., Wang, Y.: A minimalist mutual authentication protocol for RFID system and BAN logic analysis. In: Proc. ISECS Colloquium on Computing, Communication, Control and Management, pp. 449–453 (2008)
Burmester, M., Medeiros, B., Munilla, J., Peinado, A.: Secure EPC gen2 compliant radio frequency identification (2009), http://eprint.iacr.org/
Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: Proc. 22th IEEE Computer Security Foundations Symposium, pp. 157–171. IEEE Computer Society, Los Alamitos (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, X., van Deursen, T., Pang, J. (2009). Improving Automatic Verification of Security Protocols with XOR. In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-10373-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10372-8
Online ISBN: 978-3-642-10373-5
eBook Packages: Computer ScienceComputer Science (R0)