Authentication Analysis of the 802.11i Protocol

Authors: Zeeshan Furqan, Shahabuddin Muhammad, Ratan Guha

Abstract:

IEEE has designed 802.11i protocol to address the security issues in wireless local area networks. Formal analysis is important to ensure that the protocols work properly without having to resort to tedious testing and debugging which can only show the presence of errors, never their absence. In this paper, we present the formal verification of an abstract protocol model of 802.11i. We translate the 802.11i protocol into the Strand Space Model and then prove the authentication property of the resulting model using the Strand Space formalism. The intruder in our model is imbued with powerful capabilities and repercussions to possible attacks are evaluated. Our analysis proves that the authentication of 802.11i is not compromised in the presented model. We further demonstrate how changes in our model will yield a successful man-in-the-middle attack.

Keywords: authentication, formal analysis, formal verification, security.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1074529

References:

[1] R. M. Needham and M. Schroeder, "Using encryption for authentication in large networks of computers," Communications of the ACM, vol. 21, no. 12, pp. 993-999, Dec. 1978.
[2] C. Meadows, "Formal methods for cryptographic protocol analysis: Emerging issues and trends," IEEE Journal on Selected Areas in Communications, vol. 21, no. 1, pp. 44-54, Jan. 2003.
[3] F. T. Fabrega, J. Herzog, and J. Guttman, "Strand spaces: Proving security protocols correct," Journal of Computer Security, vol. 7, no. 1, pp. 191-230, 1999.
[4] N. Heintze and J. Tygar, "A model for secure protocols and their compositions," IEEE Transactions on Software Engineering, vol. 22, no. 1, pp. 16-30, Jan. 1996.
[5] I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, "A meta-notation for protocol analysis," in Proceedings of the 12th IEEE Computer Security Foundations Workshop, June 1999.
[6] G. Lowe, "Breaking and fixing the Needham-Schroeder public-key protocol using FDR," in Tools and Algorithms for the Construction and Analysis of Systems, 2nd International Workshop TACAS-96, ser. LNCS 1055. Springer Verlag, Mar. 1996, pp. 147-166.
[7] D. Dolev and A. C. Yao, "On the security of public key protocols," IEEE Transactions on Information Theory, vol. 29, pp. 198-208, Mar. 1983.
[8] D. Dolev, S. Even, and R. karp, "On the security of ping-pong protocols," Information and Control, vol. 55, no. 1-3, pp. 57-68, 1982.
[9] J. K. Millen, S. C. Clark, , and S. B. Freedman, "The interrogator: protocol security analysis," IEEE Transactions on Software Engineering, vol. 13, no. 2, pp. 274-288, Feb. 1987.
[10] R. Kemmerer, "Using formal methods to analyze encryption protocols," IEEE Journal on Selected Areas in Communications, vol. 7, no. 4, pp. 448-457, 1989.
[11] D. Longley and S. Rigby, "An automatic search for security flaws in key management schemes," Computers and Security, vol. 11, no. 1, pp. 75-90, 1992.
[12] J. C. Mitchell, M. Mitchell, and U. Stern, "Automated analysis of cryptographic protocols using Mur¤å," in Proceedings of the 1997 IEEE Symposium on Security and Privacy, May 1997, pp. 141-151.
[13] C. A. Meadows, "Analysis of the Internet Key Exchange protocol using the NRL protocol analyzer," in Proceedings of the 1999 IEEE Symposium on Security and Privacy, May 1999.
[14] D. Rosenzweig, D. Runje, and W. Schulte, "Model-based Testing of Cryptographic Protocols," in Proceedings of the IST/FET International Workshop on Trustworthy Global Computing. Springer-Verlag, Apr. 2005.
[15] E. Clarke, S. Jha, and W. Marrero, "Partial Order Reductions for Security Protocol Verification," in Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Springer-Verlag, 2000, pp. 503-518.
[16] G. Lowe, "Towards a completeness results for model checking security protocols," Journal of Computer Security, vol. 7, no. 2, 1999.
[17] R. Gumzej, M. Colnaric, and W. Halang, "Temporal feasibility verification of specification PEARL designs," in Proceedings of the Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing. IEEE Computer Society Press, May 2004, pp. 249- 252.
[18] M. Burrows, M. Abadi, and R. Needham, "A logic of authentication," ACM Transactions on Computer Systems, vol. 8, no. 1, pp. 18-36, Feb. 1990.
[19] L. Gong, R. Needham, and R. Yahalom, "Reasoning about belief in cryptographic protocols," in Proceedings of the IEEE Symposium on Research in Security and Privacy, May 1990, pp. 234-248.
[20] P. Syverson and P. V. Oorschot, "On unifying some cryptographic protocol logics," in Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, 1994, pp. 14-28.
[21] W. Diffie and M. Hellman, "New directions in cryptography," IEEE Transactions on Information Theory, vol. 22, no. 6, pp. 644-654, 1976.
[22] L. C. Paulson, "The inductive approach to verifying cryptographic protocols," Journal of Computer Security, vol. 6, pp. 85-128, 1998.
[23] S. Brackin, "Evaluating and Improving Protocol Analysis by Automatic Proof," in Proceedings of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, June 1998, pp. 138-152.
[24] J. Heather and S. Schneider, "Towards automatic verification of authentication protocols on an unbounded network," in Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, June 2000.
[25] E. Cohen, "TAPS: a first-order verifier for cryptographic protocols," in Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, June 2000, pp. 144-158.
[26] M. Abadi, "Secrecy by typing in security protocols," Journal of the ACM, vol. 46, no. 5, pp. 749-786, Sept. 1999.
[27] M. Abadi and P. Rogaway., "Reconciling two views of cryptography (the computational soundeness of formal encryption)," Journal of Cryptology, vol. 15, no. 2, pp. 103-127, Jan. 2002.
[28] J. Y. Halpern and R. Pucella, "On the relationship between strand spaces and multi-agent systems," ACM Transactions on Information and System Security, vol. 6, no. 1, pp. 43-70, 2003.
[29] Q. Ji, S. Qing, Y. Zhou, and D. Feng, "Study on strand space model theory," Journal of Computer Science and Technology, vol. 18, no. 5, pp. 553-570, 2003.
[30] C. Caleiro, L. Vigano, and D. Basin, "Relating strand spaces and distributed temporal logic for security protocol analysis," Logic Journal of the IGPL, vol. 13, no. 6, pp. 637-664, 2005.
[31] D. Song, S. Berezin, and A. Perrig, "Athena: a novel approach to efficient automatic security protocol analysis," Journal of Computer Security, vol. 9, pp. 47-74, 2001.
[32] G. Lowe, "A hierarchy of authentication specification," in Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy, 1997, pp. 31-43.
[33] B. Aboba, L. Blunk, J. Vollbrecht, J. Carlson, and H. E. Levkowetz, "Extensible authentication protocol EAP. RFC 3748," June 2004.
[34] C. Rigney, A. Rubens, W. Simpson, and S. Willens, "Remote authentication dial in user service (RADIUS). RFC 2138," Apr. 1997.