Myrto Arapinis
ABSTRACT
Mobile telephony equipment is daily carried by billions of subscribers everywhere they go. Avoiding linkability of subscribers by third parties, and protecting the privacy of those subscribers is one of the goals of mobile telecommunication protocols. We use formal methods to model and analyse the security properties of 3G protocols. We expose two novel threats to the user privacy in 3G telephony systems, which make it possible to trace and identify mobile telephony subscribers, and we demonstrate the feasibility of a low cost implementation of these attacks. We propose fixes to these privacy issues, which also take into account and solve other privacy attacks known from the literature. We successfully prove that our privacy-friendly fixes satisfy the desired unlinkability and anonymity properties using the automatic verification tool ProVerif.
- http://www.pathintelligence.com. Path Intelligence Ltd. (2010) FootPath.Google Scholar
- http://www.markryan.eu/research/UMTS/.Google Scholar
- 3GPP. Technical specification group services and system aspects; 3G security; formal analysis of the 3G authentication protocol (release 4). Technical Report TR 33.902, V4.0.0, 3rd Generation Partnership Project, 2001.Google Scholar
- 3GPP. Generic Access Network (GAN); Mobile GAN interface layer 3 specification. Technical Specification TS 44.318 v9.2.0, 3rd Generation Partnership Project, 2010.Google Scholar
- 3GPP. Generic Access Network (GAN); Stage 2. Technical Specification TS 43.318 v9.0.0, 3rd Generation Partnership Project, 2010.Google Scholar
- 3GPP. Technical specification group services and system aspects; 3G security; security architecture (release 9). Technical Report TS 33.102 V9.3.0, 3rd Generation Partnership Project, 2010.Google Scholar
- 3GPP. Security of Home Node B (HNB) / Home evolved Node B (HeNB). Technical Specification TS 33.302 v11.2.0, 3rd Generation Partnership Project, 2011.Google Scholar
- 3GPP. Technical specification group services and system aspects; 3G security; cryptographic algorithm requirements (release 10). Technical Report TS 33.105 V10.0.0, 3rd Generation Partnership Project, 2011.Google Scholar
- M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2001. Google ScholarDigital Library
- Z. Ahmadian, S. Salimi, and A. Salahi. New attacks on UMTS network access. In Conference on Wireless Telecommunications Symposium, WTS'09, 2009. Google ScholarDigital Library
- M. Arapinis, T. Chothia, E. Ritter, and M. Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In IEEE Computer Security Foundations Symposium, CSF, 2010. Google ScholarDigital Library
- A. Armando, R. Carbone, L. Compagna, J. Cuellar, and M. L. Tobarra. Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps. In ACM Workshop on Formal Methods in Security Engineering, FMSE, 2008. Google ScholarDigital Library
- G. Avoine and P. Oechslin. RFID Traceability: A Multilayer Problem. In Financial Cryptography, FC, 2005. Google ScholarDigital Library
- M. Barbaro and T. Zeller Jr. A face is exposed for AOL searcher no. 4417749. The New York Times, August 9, 2006.Google Scholar
- B. Blanchet. Proverif: Cryptographic protocol verifier in the formal model. http://www.proverif.ens.fr/.Google Scholar
- M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel. Attacking and fixing PKCS#11 security tokens. In ACM Conference on Computer and Communications Security, CCS, 2010. Google ScholarDigital Library
- C. Caldwell. A pass on privacy? The New York Times, July 17, 2005.Google Scholar
- I. Cervesato, A. D. Jaggard, A. Scedrov, J.-K. Tsay, and C. Walstad. Breaking and fixing public-key kerberos. Inf. Comput., 206:402--424, February 2008. Google ScholarDigital Library
- D. Burgess et al. OpenBTS. http://openbts.sourceforge.net/.Google Scholar
- N. H. Denis Foo Kune, John Koelndorfer and Y. Kim. Location leaks over the gsm air interface. In Annual Network & Distributed System Security Symposium, NDSS, 2012.Google Scholar
- Ettus. USRP. http://www.ettus.com/products, 2009.Google Scholar
- D. Fox. IMSI-Catcher. Datenschutz und Datensicherheit (DuD), 21:539--539, 1997.Google Scholar
- N. Golde, K. Redon, and R. Borgaonkar. Weaponizing femtocells: The effect of rogue devices on mobile telecommunications. In Annual Network & Distributed System Security Symposium, NDSS, 2012.Google Scholar
- D. Goodin. Defects in e-passports allow real-time tracking. The Register, 26th January 2010.Google Scholar
- Kineto Wireless Inc. official Unlicensed Mobile Access presentation webiste. http://www.smart-wi-fi.com/, June 2010.Google Scholar
- G. Koien and V. Oleshchuk. Location privacy for cellular systems; analysis and solution. In Privacy Enhancing Technologies Symposium, volume 3856, 2006. Google ScholarDigital Library
- G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using fdr. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 1996. Google ScholarDigital Library
- U. Meyer and S. Wetzel. A man-in-the-middle attack on UMTS. In ACM Workshop on Wireless Security, WiSe, 2004. Google ScholarDigital Library
- K. Nohl and S. Munaut. Wideband gsm sniffing. http://events.ccc.de/congress/2010/Fahrplan/attachments/1783_101228.27C3.GSM-Sniffing.Nohl_Munaut.pdf.Google Scholar
- openBSC Project. GSM Network at 28C3. http://events.ccc.de/congress/2011/wiki/GSM#GSM_Network_at_28C3, December 2011.Google Scholar
- C. Paget. Practical cellphone spying. Def Con 18 Hacking Conference, 2010.Google Scholar
- D. Strobel. IMSI Catcher, 2007. Seminar Work, Ruhr-Universitat Bochum.Google Scholar
- H. Welte, H. Freyther, D. Spaar, S. Schmidt, D. Willmann, J. Luebbe, T. Seiler, and A. Eversberg. OpenBSC. http://openbsc.osmocom.org.Google Scholar
- H. Welte, S. Munaut, A. Eversberg, and other contributors. OsmocomBB. http://bb.osmocom.org.Google Scholar
- J. Zhang and G. de la Roche. Femtocells: Technologies and Deployment. John Wiley & Sons, Ltd, 2009. Google ScholarDigital Library
- M. Zhang and Y. Fang. Security analysis and enhancements of 3GPP authentication and key agreement protocol. IEEE Transactions on Wireless Communications, 4(2):734--742, 2005. Google ScholarDigital Library
Index Terms
- New privacy issues in mobile telephony: fix and verification
Recommendations
Analysis of privacy in mobile telephony systems
We present a thorough experimental and formal analysis of users' privacy in mobile telephony systems. In particular, we experimentally analyse the use of pseudonyms and point out weak deployed policies leading to some critical scenarios which make it ...
An Unlinkable Anonymous Payment Scheme based on near field communication
Display Omitted We propose an anonymous mobile payment protocol to protect users' privacy.Using anonymizing schemes to improve anonymity and unlinkability in a mobile transaction.Users can use mobile phones with NFC to perform commercial transactions. A ...
The security of EPC Gen2 compliant RFID protocols
ACNS'08: Proceedings of the 6th international conference on Applied cryptography and network securityThe increased functionality of EPC Class1 Gen2 (EPCGen2) is making this standard the de facto specification for inexpensive tags in the RFID industry. EPCGen2 supports only very basic security tools such as a 16-bit Pseudo-Random Number Generator and a ...
Comments