Authentication Analysis of the 802.11i Protocol

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.

Authors:

• Zeeshan Furqan
• Shahabuddin Muhammad
• Ratan Guha

Keywords:

• authentication
• formal analysis
• formal verification
• security.

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.