Abstract
Wi-Fi Protected Setup is an attempt to simplify configuration of security settings for Wi-Fi networks. It offers, among other methods, Push-Button ConfigurationĀ (PBC) for devices with a limited user-interface. There are however some security issues in PBC. A solution to these issues was proposed in the form of Tamper-Evident PairingĀ (TEP).
TEP is based on the Tamper-Evident Announcement (TEA), in which a device engaging in the key agreement not only sends a payload containing its Diffie-Hellmann public key, but also sends a hash of this payload in a special, trustedly secure manner. The idea is that thanks to the special way in which the hash is sent, the receiver can tell whether or not the hash was altered by an adversary and if necessary reject it.
Several parameters needed for implementation of TEP have been left unspecified by its authors. Verification of TEA using the Spin model-checker has revealed that the value of these parameters is critical for the security of the protocol. The implementation decision can break the resistance of TEP against man-in-the-middle attacks. We give appropriate values for these parameters and show how model-checking was applied to retrieve these values.
This work is part of the IOP GenCom GoGreen project, sponsored by the Dutch Ministry of Economic Affairs, Agriculture and Innovation.
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
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., HeĆ”m, P.C., Kouchnarenko, O., Mantovani, J., Mƶdersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., ViganĆ², L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.Ā 3576, pp. 281ā285. Springer, Heidelberg (2005)
Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. Journal of Applied Non-Classical LogicsĀ 19(4), 403ā429 (2009)
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: uppaal ā a Tool Suite for Automatic Verification of RealāTime Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.Ā 1066, pp. 232ā243. Springer, Heidelberg (1996)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, pp. 82ā96. IEEE Computer Society (June 2001)
BoŔnacki, D., Dams, D.: Integrating real time into Spin: a prototype implementation. In: BoŔnacki, D. (ed.) Enhancing State Space Reduction Techniques for Model Checking. Technische Universiteit Eindhoven (1998)
Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information TheoryĀ 22(6), 644ā654 (1976)
Drijvers, M.: Model checking Tamper-Evident Pairing. Bachelor thesis, Radboud University Nijmegen (2012)
Gollakota, S., Ahmed, N., Zeldovich, N., Katabi, D.: Secure in-band wireless pairing. In: Proceedings of the 20th USENIX Conference on Security, SEC 2011. USENIX Association, Berkeley (2011)
Holzmann, G.: The model checker Spin. IEEE Transactions on Software EngineeringĀ 23(5), 279ā295 (1997)
Kainda, R., Flechais, I., Roscoe, A.W.: Usability and security of out-of-band channels in secure device pairing protocols. In: Proceedings of the 5th Symposium on Usable Privacy and Security, pp. 11:1ā11:12. ACM, New York (2009)
Kobsa, A., Sonawalla, R., Tsudik, G., Uzun, E., Wang, Y.: Serial hook-ups: a comparative usability study of secure device pairing methods. In: Proceedings of the 5th Symposium on Usable Privacy and Security, pp. 10:1ā10:12. ACM, New York (2009)
Kuo, C., Walker, J., Perrig, A.: Low-cost manufacturing, usability, and security: An analysis of Bluetooth Simple Pairing and Wi-Fi Protected Setup. In: Dietrich, S., Dhamija, R. (eds.) FC 2007 and USEC 2007. LNCS, vol.Ā 4886, pp. 325ā340. Springer, Heidelberg (2007)
Lowe, G.: Towards a completeness result for model checking of security protocols. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop, pp. 96ā105 (June 1998)
Martin, M., Lam, M.S.: Automatic generation of XSS and SQL injection attacks with goal-directed model checking. In: Proceedings of the 17th Conference on Security Symposium, SS 2008, pp. 31ā43. USENIX Association (2008)
Martinelli, F.: Partial model checking and theorem proving for ensuring security properties. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop, pp. 44ā52 (1998)
Mayrhofer, R., Gellersen, H.: On the security of ultrasound as out-of-band channel. In: IEEE International Parallel and Distributed Processing Symposium, IPDPS 2007, pp. 1ā6 (March 2007)
Mayrhofer, R., Gellersen, H., Hazas, M.: Security by spatial reference: Using relative positioning to authenticate devices for spontaneous interaction. In: Krumm, J., Abowd, G.D., Seneviratne, A., Strang, T. (eds.) UbiComp 2007. LNCS, vol.Ā 4717, pp. 199ā216. Springer, Heidelberg (2007)
Mayrhofer, R., Welch, M.: A human-verifiable authentication protocol using visible laser light. In: The Second International Conference on Availability, Reliability and Security, ARES 2007, pp. 1143ā1148 (April 2007)
Ritchey, R., Ammann, P.: Using model checking to analyze network vulnerabilities. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy, S P 2000, pp. 156ā165 (2000)
Saxena, N., Ekberg, J.-E., Kostiainen, K., Asokan, N.: Secure device pairing based on a visual channel. In: 2006 IEEE Symposium on Security and Privacy, pp. 306ā313 (May 2006)
Schwarz, B., Chen, H., Wagner, D., Morrison, G., West, J., Lin, J., Tu, W.: Model checking an entire Linux distribution for security violations. In: 21st Annual Computer Security Applications Conference, pp. 10ā22 (2005)
Smetters, D.B., Balfanz, D., Smetters, D.K., Stewart, P., Wong, H.C.: Talking to strangers: Authentication in ad-hoc wireless networks (2002)
Stajano, F., Anderson, R.: The resurrecting duckling: security issues for ubiquitous computing. ComputerĀ 35(4), 22ā26 (2002)
Suomalainen, J., Valkonen, J., Asokan, N.: Security associations in personal networks: A comparative analysis. In: Stajano, F., Meadows, C., Capkun, S., Moore, T. (eds.) ESAS 2007. LNCS, vol.Ā 4572, pp. 43ā57. Springer, Heidelberg (2007)
Viehbƶck, S.: Brute forcing Wi-Fi protected setup, http://sviehb.files.wordpress.com/2011/12/viehboeck_wps.pdf
Ware, C., Judge, J., Chicharo, J., Dutkiewicz, E.: Unfairness and capture behaviour in 802.11 adhoc networks. In: 2000 IEEE International Conference on Communications, ICC 2000, vol.Ā 1, pp. 159ā163 (2000)
Wi-Fi Alliance: Wi-Fi Protected Setup Specification, version 1.0h (2006)
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
Kersten, R., van Gastel, B., Drijvers, M., Smetsers, S., van Eekelen, M. (2013). Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing. In: Brat, G., Rungta, N., Venet, A. (eds) NASA Formal Methods. NFM 2013. Lecture Notes in Computer Science, vol 7871. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38088-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-38088-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38087-7
Online ISBN: 978-3-642-38088-4
eBook Packages: Computer ScienceComputer Science (R0)