Abstract
The EAP-GPSK protocol is a lightweight, flexible authentication protocol relying on symmetric key cryptography. It is part of an ongoing IETF process to develop authentication methods for the EAP framework. We analyze the protocol and find three weaknesses: a repairable Denial-of-Service attack, an anomaly with the key derivation function used to create a short-term master session key, and a ciphersuite downgrading attack. We propose fixes to these anomalies, and use a finite-state verification tool to search for remaining problems after making these repairs. We then prove the fixed version correct using a protocol verification logic. We discussed the attacks and our suggested fixes with the authors of the specification document which has subsequently been modified to include our proposed changes.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aboba, B., Blunk, L., Vollbrecht, J., Carlson, J.: Extensible Authentication Protocol. RFC 3748 (2004)
Clancy, T., Tschofenig, H.: EAP Generalized Pre-Shared Key (EAP-GPSK) (work in progress) (2007), http://www.ietf.org/internet-drafts/draft-ietf-emu-eap-gpsk-05.txt
Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 16–29. Springer, Heidelberg (2005)
Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321–334. IEEE, Los Alamitos (2006)
Dill, D.L.: The Murφ Verification System. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 147–158. Springer, Heidelberg (1996)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols Using Murφ. In: IEEE Symposium on Security and Privacy, pp. 141–151 (1997)
Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-State Analysis of SSL 3.0. In: SSYM 1998: Proceedings of the 7th conference on USENIX Security Symposium, 1998, Berkeley, CA, USA, pp. 16–16. USENIX Association (1998)
He, C., Mitchell, J.C.: Analysis of the 802.11i 4-Way Handshake. In: WiSe 2004: Proceedings of the 3rd ACM Workshop on Wireless Security, pp. 43–50. ACM, New York (2004)
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electron. Notes Theor. Comput. Sci. 172, 311–358 (2007)
Meadows, C.: A model of computation for the NRL protocol analyzer. In: Proceedings of 7th IEEE Computer Security Foundations Workshop, pp. 84–89. IEEE, Los Alamitos (1994)
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, A.: Modelling and Analysis of Security Protocols. Addison-Wesley Publishing Co., Reading (2000)
Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, Oakland, CA, pp. 160–171. IEEE Computer Society Press, Los Alamitos (1998)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361–375. Springer, Heidelberg (1998)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A Formal Analysis of Some Properties of Kerberos 5 Using MSR. In: Fifteenth Computer Security Foundations Workshop — CSFW-15, Cape Breton, NS, Canada, pp. 175–190. IEEE Computer Society Press, Los Alamitos (2002)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: Verifying confidentiality and authentication in kerberos 5. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 1–24. Springer, Heidelberg (2004)
Cervesato, I., Jaggard, A., Scedrov, A., Tsay, J.K., Walstad, C.: Breaking and fixing public-key kerberos (Technical report)
Cervasato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution. In: CSFW-18, IEEE Computer Society, Los Alamitos (2005)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13, 423–482 (2005)
Hasebe, K., Okada, M.: Non-monotonic properties for proving correctness in a framework of compositional logic. In: Foundations of Computer Security Workshop, pp. 97–113 (2004)
Hasebe, K., Okada, M.: Inferences on honesty in compositional logic for security analysis. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 65–86. Springer, Heidelberg (2004)
He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of ieee 802.11i and tls. In: ACM Conference on Computer and Communications Security, pp. 2–15 (2005)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15, 103–127 (2002)
Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. Cryptology ePrint Archive, Report 2003/015 (2003)
Baudet, M., Cortier, V., Kremer, S.: Computationally Sound Implementations of Equational Theories against Passive Adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005)
Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)
Herzog, J.: Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT (2004)
Adão, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. CSFW 18, 170–184 (2005)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Warinschi, B.: A computational analysis of the Needham-Schroeder(-Lowe) protocol. In: Proceedings of 16th Computer Science Foundation Workshop, pp. 248–262. ACM Press, New York (2003)
Roy, A., Datta, A., Derek, A., Mitchell, J.C., Seifert, J.P.: Secrecy analysis in Protocol Composition Logic. In: Proceedings of 11th Annual Asian Computing Science Conference (to appear, 2006)
Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 219–234. Springer, Heidelberg (2007)
Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie-Hellman-based protocols. In: 3rd Symposium on Trustworthy Global Computing, TGC 2007. LNCS, vol. 4912, pp. 312–329. Springer, Heidelberg (2008)
Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive trace properties for computational security. In: WITS (2007)
Dierks, T., Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346 (2006)
Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited (preliminary version). In: STOC 1998: Proceedings of the thirtieth annual ACM symposium on Theory of computing, pp. 209–218. ACM, New York (1998)
Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for protocol correctness. In: Proceedings of 14th IEEE Computer Security Foundations Workshop, pp. 241–255. IEEE, Los Alamitos (2001)
Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for proving security properties of protocols. Journal of Computer Security 11, 677–721 (2003)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system for security protocols and its logical formalization. In: CSFW-16, pp. 109–125. IEEE, Los Alamitos (2003)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Secure protocol composition. In: Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 83 (2004)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: CSFW-17, pp. 30–45. IEEE, Los Alamitos (2004)
Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mitchell, J.C., Roy, A., Rowe, P., Scedrov, A. (2008). Analysis of EAP-GPSK Authentication Protocol. In: Bellovin, S.M., Gennaro, R., Keromytis, A., Yung, M. (eds) Applied Cryptography and Network Security. ACNS 2008. Lecture Notes in Computer Science, vol 5037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68914-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-68914-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68913-3
Online ISBN: 978-3-540-68914-0
eBook Packages: Computer ScienceComputer Science (R0)