×

A process calculus for privacy-preserving protocols in location-based service systems. (English) Zbl 07485816

Summary: Location privacy-preserving mechanisms (LPPM) were introduced to protect users of location-based services (LBS) from the privacy threat of leaked personal data. These mechanisms alter the communication to the LBS in such a way that no malicious party can derive sensitive personal data. In the literature one can find many different LPPMs with varying privacy guarantees but so far no formal framework exists for comparing all of these mechanisms and their privacy guarantees. We propose the \(\sigma \)-calculus, which enables the modeling of LPPMs and location privacy guarantees. The calculus entails a process language, a property language, and a temporal-K-less-epistemic modal logic that enables the verification of location privacy properties on process models. The \(\sigma \)-calculus is a novel process calculus that is based on standard set operations that are computationally cheap, yet sufficient for modeling privacy violations in LBS communication. The calculus is the first formal framework to model and reason about a wide array of LPPMs. Furthermore, we present model checking algorithms that enable the automatic verification of location privacy properties. We evaluate the expressiveness of our process language by modeling a significant number of LPPMs from the literature and the expressiveness of our property language by describing a benchmark set of location privacy properties. Furthermore, we demonstrate the verification of a privacy property with an extended example of an LPPM algorithm designer. We developed the tool LP3Verif that implements our model checking algorithms. The open-source tool is written in Java and uses the SMT solver CVC4 as back end.

MSC:

68-XX Computer science
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Agir, Berker; Papaioannou, Thanasis G.; Narendula, Rammohan; Aberer, Karl; Hubaux, Jean-Pierre, User-side adaptive protection of location privacy in participatory sensing, GeoInformatica, 18, 1, 165-191 (January 2014)
[2] Matchi Aïvodji, Ulrich; Huguenin, Kévin; Huguet, Marie-José; Killijian, Marc-Olivier, SRide: a privacy-preserving ridesharing system, (Proceedings of the 11th ACM Conference on Security & Privacy in Wireless and Mobile Networks. Proceedings of the 11th ACM Conference on Security & Privacy in Wireless and Mobile Networks, WiSec ’18, Stockholm, Sweden (June 2018), Association for Computing Machinery), 40-50
[3] Anderson, Gabrielle; Pym, David, A calculus and logic of bunched resources and processes, Theor. Comput. Sci., 614, 63-96 (February 2016)
[4] Andrés, Miguel E.; Bordenabe, Nicolás E.; Chatzikokolakis, Konstantinos; Palamidessi, Catuscia, Geo-indistinguishability: differential privacy for location-based systems, (Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security. Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, CCS ’13, Berlin, Germany (November 2013), Association for Computing Machinery), 901-914
[5] Antignac, Thibaud; Le Métayer, Daniel, Trust driven strategies for privacy by design, (IFIP Advances in Information and Communication Technology (2015), Springer International Publishing: Springer International Publishing Cham), 60-75
[6] Assam, Roland; Seidl, Thomas, Preserving privacy of moving objects via temporal clustering of spatio-temporal data streams, (Proceedings of the 4th ACM SIGSPATIAL International Workshop on Security and Privacy in GIS and LBS. Proceedings of the 4th ACM SIGSPATIAL International Workshop on Security and Privacy in GIS and LBS, SPRINGL ’11, Chicago, Illinois (November 2011), Association for Computing Machinery), 9-16
[7] Baeten, Jos C. M., A brief history of process algebra, Theor. Comput. Sci., 335, 2-3, 131-146 (May 2005)
[8] Bamba, Bhuvan; Liu, Ling; Pesti, Peter; Wang, Ting, Supporting anonymous location queries in mobile environments with PrivacyGrid, (Proceeding of the 17th International Conference on World Wide Web. Proceeding of the 17th International Conference on World Wide Web, WWW ’08, Beijing, China (2008), ACM Press), 237
[9] Beresford, Alastair R.; Stajano, Frank, Mix zones: user privacy in location-aware services, (Proceedings of the Second IEEE Annual Conference on Pervasive Computing and Communications Workshops, 2004 (March 2004)), 127-131
[10] Bindschaedler, Vincent; Shokri, Reza, Synthesizing plausible privacy-preserving location traces, (2016 IEEE Symposium on Security and Privacy (SP) (May 2016)), 546-563
[11] Blanchet, Bruno; Abadi, Martín; Fournet, Cédric, Automated verification of selected equivalences for security protocols, J. Log. Algebraic Program., 75, 1, 3-51 (February 2008)
[12] Bordenabe, Nicolás E.; Chatzikokolakis, Konstantinos; Palamidessi, Catuscia, Optimal geo-indistinguishable mechanisms for location privacy, (Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, Scottsdale, Arizona, USA (November 2014), Association for Computing Machinery), 251-262
[13] Braubach, Lars; van der Hoek, Wiebe; Petta, Paolo; Pokahr, Alexander; Delgado, Carla; Benevides, Mario, Verification of Epistemic Properties in Probabilistic Multi-Agent Systems (2009), Springer: Springer Berlin, Heidelberg
[14] Cardelli, Luca; Gordon, Andrew D., Anytime, anywhere: modal logics for mobile ambients, (Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’00. Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’00, Boston, MA, USA (2000), ACM Press), 365-377 · Zbl 1323.68405
[15] Carter, Henry; Mood, Benjamin; Traynor, Patrick; Butler, Kevin, Secure outsourced garbled circuit evaluation for mobile devices, J. Comput. Secur., 24, 2, 137-180 (April 2016)
[16] Chadha, Rohit; Delaune, Stéphanie; Kremer, Steve, Epistemic logic for the applied pi calculus, (Lee, David; Lopes, Antónia; Poetzsch-Heffter, Arnd, Formal Techniques for Distributed Systems, vol. 5522 (2009), Springer: Springer Berlin, Heidelberg), 182-197
[17] Supriyo Chakraborty, Chenguang Shen, Kasturi Rangan Raghavan, Matt Millar, Mani Srivastava, ipShield: a Framework for Enforcing Context-Aware Privacy on Android, page 13.
[18] Konstantinos Chatzikokolakis, Catuscia Palamidessi, Marco Stronati, Location Guard: Location privacy for the rest of us. · Zbl 1471.68090
[19] Chatzikokolakis, Konstantinos; Palamidessi, Catuscia; Stronati, Marco, A predictive differentially-private mechanism for mobility traces (June 2014)
[20] Chatzikokolakis, Konstantinos; Palamidessi, Catuscia; Stronati, Marco, Constructing elastic distinguishability metrics for location privacy, Proc. Priv. Enhancing Technol., 2015, 2, 156-170 (June 2015)
[21] Chow, Chi-Yin; Mokbel, Mohamed F.; Liu, Xuan, A peer-to-peer spatial cloaking algorithm for anonymous location-based services, page 8
[22] Chow, Chi-Yin; Mokbel, Mohamed F.; Aref, Walid G., Casper*: query processing for location services without compromising privacy, ACM Trans. Database Syst., 34, 4, 24:1-24:48 (December 2009)
[23] Ding, Jingquan; Li, Xiao; Guo, Yunchuan; Yin, Lihua; Zhang, Huibing, Process calculus for modeling and quantifying location privacy, Proc. Comput. Sci., 147, 407-415 (January 2019)
[24] Fawaz, Kassem; Shin, Kang G., Location privacy protection for smartphone users, (Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, Scottsdale, Arizona, USA (November 2014), Association for Computing Machinery), 239-250
[25] Freudiger, Julien; Shokri, Reza; Hubaux, Jean-Pierre, On the optimal placement of mix zones, (Goldberg, Ian; Atallah, Mikhail J., Privacy Enhancing Technologies. Privacy Enhancing Technologies, Berlin, Heidelberg. Privacy Enhancing Technologies. Privacy Enhancing Technologies, Berlin, Heidelberg, Lecture Notes in Computer Science (2009), Springer), 216-234
[26] Gedik, Bugra; Liu, Ling, Location privacy in mobile systems: a personalized anonymization model, (25th IEEE International Conference on Distributed Computing Systems. 25th IEEE International Conference on Distributed Computing Systems, ICDCS’05 (June 2005)), 620-629
[27] Ghinita, Gabriel; Kalnis, Panos; Skiadopoulos, Spiros, PRIVE: anonymous location-based queries in distributed mobile systems, (Proceedings of the 16th International Conference on World Wide Web. Proceedings of the 16th International Conference on World Wide Web, WWW ’07, Banff, Alberta, Canada (2007), ACM Press), 371-380
[28] Ghinita, Gabriel; Kalnis, Panos; Khoshgozaran, Ali; Shahabi, Cyrus; Tan, Kian-Lee, Private queries in location based services: anonymizers are not necessary, (Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data. Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data, SIGMOD ’08, Vancouver, Canada (June 2008), Association for Computing Machinery), 121-132
[29] Gong, Xiaowen; Chen, Xu; Xing, Kai; Shin, Dong-Hoon; Zhang, Mengyuan; Zhang, Junshan, From social group utility maximization to personalized location privacy in mobile networks, IEEE/ACM Trans. Netw., 25, 3, 1703-1716 (June 2017)
[30] Guha, Saikat; Jain, Mudit; Padmanabhan, Venkata N., Koi: a location-privacy platform for smartphone apps, (Presented as Part of the 9th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 12) (2012)), 183-196
[31] Halpern, Joseph Y.; vander Meyden, Ron; Vardi, Moshe Y., Complete axiomatizations for reasoning about knowledge and time, SIAM J. Comput., 33, 3, 674-703 (2004) · Zbl 1059.68127
[32] Hintikka, Jaakko, Knowledge and belief: an introduction to the logic of the two notions, Stud. Log., 16, 119-122 (1962)
[33] Hoh, Baik; Gruteser, Marco; Xiong, Hui; Alrabady, Ansaf, Preserving privacy in GPS traces via uncertainty-aware path cloaking, (Proceedings of the 14th ACM Conference on Computer and Communications Security. Proceedings of the 14th ACM Conference on Computer and Communications Security, CCS ’07, Alexandria, Virginia, USA (October 2007), Association for Computing Machinery), 161-171
[34] Huguenin, Kévin; Bilogrevic, Igor; Soares Machado, Joana; Mihaila, Stefan; Shokri, Reza; Dacosta, Italo; Hubaux, Jean-Pierre, A predictive model for user motivation and utility implications of privacy-protection mechanisms in location check-ins, IEEE Trans. Mob. Comput., 17, 4, 760-774 (April 2018)
[35] Huth, Michael; Ryan, Mark, Logic in Computer Science: Modelling and Reasoning About Systems (August 2004), Cambridge University Press
[36] Jaiswal, Sharad; Nandi, Animesh, Trust no one: a decentralized matching service for privacy in location based services, (Proceedings of the Second ACM SIGCOMM Workshop on Networking, Systems, and Applications on Mobile Handhelds. Proceedings of the Second ACM SIGCOMM Workshop on Networking, Systems, and Applications on Mobile Handhelds, MobiHeld ’10, New Delhi, India (August 2010), Association for Computing Machinery), 51-56
[37] Kato, Ryo; Iwata, Mayu; Hara, Takahiro; Suzuki, Akiyoshi; Xie, Xing; Arase, Yuki; Nishio, Shojiro, A dummy-based anonymization method based on user trajectory with pauses, (Proceedings of the 20th International Conference on Advances in Geographic Information Systems. Proceedings of the 20th International Conference on Advances in Geographic Information Systems, SIGSPATIAL ’12, Redondo Beach, California (November 2012), Association for Computing Machinery), 249-258
[38] Kido, Hidetoshi; Yanagisawa, Yutaka; Satoh, Tetsuji, Protection of location privacy using dummies for location-based services, (21st International Conference on Data Engineering Workshops. 21st International Conference on Data Engineering Workshops, ICDEW’05 (April 2005)), 1248
[39] Krumm, John, Realistic driving trips for location privacy, (Tokuda, Hideyuki; Beigl, Michael; Friday, Adrian; Bernheim Brush, A. J.; Tobe, Yoshito, Pervasive Computing, Lecture Notes in Computer Science (2009), Springer: Springer Berlin, Heidelberg), 25-41
[40] Krumm, John, A survey of computational location privacy, Pers. Ubiquitous Comput., 13, 6, 391-399 (August 2009)
[41] Lee, Hyun-Jo; Hong, Seung-Tae; Yoon, Min; Um, Jung-Ho; Chang, Jae-Woo, A new cloaking algorithm using Hilbert curves for privacy protection, (Proceedings of the 3rd ACM SIGSPATIAL International Workshop on Security and Privacy in GIS and LBS. Proceedings of the 3rd ACM SIGSPATIAL International Workshop on Security and Privacy in GIS and LBS, SPRINGL ’10, San Jose, California (November 2010), Association for Computing Machinery), 42-46
[42] Li, Chao; Palanisamy, Balaji, ReverseCloak: protecting multi-level location privacy over road networks, (Proceedings of the 24th ACM International on Conference on Information and Knowledge Management. Proceedings of the 24th ACM International on Conference on Information and Knowledge Management, CIKM ’15, Melbourne, Australia (2015), ACM Press), 673-682
[43] Liu, Xinxin; Zhao, Han; Pan, Miao; Yue, Hao; Li, Xiaolin; Fang, Yuguang, Traffic-aware multiple mix zone placement for protecting location privacy, (2012 Proceedings IEEE INFOCOM (March 2012)), 972-980
[44] Mascetti, Sergio; Freni, Dario; Bettini, Claudio; Wang, X. Sean; Jajodia, Sushil, Privacy in geo-social networks: proximity notification with untrusted service providers and curious buddies, VLDB J., 20, 4, 541-566 (August 2011)
[45] Kristopher Micinski, Philip Phelps, Jeffrey S. Foster, An Empirical Study of Location Truncation on Android.
[46] Milner, Robin; Parrow, Joachim; Walker, David, A calculus of mobile processes, I, Inf. Comput., 100, 1, 1-40 (September 1992)
[47] Mohamed, F.; Mokbel; Chow, Chi-Yin; Aref, Walid G., The new Casper: query processing for location services without compromising privacy, (Proceedings of the 32nd International Conference on Very Large Data Bases (2006)), 763-774
[48] Murphy, T.; Crary, K.; Harper, R.; Pfenning, F., A symmetric modal lambda calculus for distributed computing, (Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004 (July 2004)), 286-295
[49] Arvind Narayanan, Narendran Thiagarajan, Mugdha Lakhani, Michael Hamburg, Dan Boneh, Location Privacy via Private Proximity Testing, page 17.
[50] Ngo, Hoa; Kim, Jong, Location privacy via differential private perturbation of cloaking area, (2015 IEEE 28th Computer Security Foundations Symposium (July 2015)), 63-74
[51] Niu, Ben; Li, Qinghua; Zhu, Xiaoyan; Cao, Guohong; Li, Hui, Enhancing privacy through caching in location-based services, (2015 IEEE Conference on Computer Communications (INFOCOM) (April 2015)), 1017-1025
[52] Oya, Simon; Troncoso, Carmela; Pérez-González, Fernando, Back to the drawing board: revisiting the design of optimal location privacy-preserving mechanisms, (Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, Dallas, Texas, USA (October 2017), Association for Computing Machinery), 1959-1972
[53] Balaji, Palanisamy; Liu, Ling, MobiMix: protecting location privacy with mix-zones over road networks, (2011 IEEE 27th International Conference on Data Engineering (April 2011)), 494-505
[54] Sarah Pidcock, Urs Hengartner, Zerosquare: a Privacy-Friendly Location Hub for Geosocial Applications.
[55] Pingley, Aniket; Yu, Wei; Zhang, Nan; Fu, Xinwen; Zhao, Wei, CAP: a context-aware privacy protection system for location-based services, (2009 29th IEEE International Conference on Distributed Computing Systems (June 2009)), 49-57
[56] Ada Popa, Raluca; Blumberg, Andrew J.; Balakrishnan, Hari; Li, Frank H., Privacy and accountability for location-based aggregate statistics, (Proceedings of the 18th ACM Conference on Computer and Communications Security. Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS ’11, Chicago, Illinois, USA (October 2011), Association for Computing Machinery), 653-666
[57] Quercia, Daniele; Leontiadis, Ilias; McNamara, Liam; Mascolo, Cecilia; Crowcroft, Jon, SpotME if you can: randomized responses for location obfuscation on mobile phones, (2011 31st International Conference on Distributed Computing Systems (June 2011)), 363-372
[58] Ryan, Mark Dermot; Smyth, Ben, Applied pi calculus, (Formal Models and Techniques for Analyzing Security Protocols, vol. 5 (2011)), 112-142
[59] Shankar, Pravin; Ganapathy, Vinod; Iftode, Liviu, Privately querying location-based services with SybilQuery, (Proceedings of the 11th International Conference on Ubiquitous Computing. Proceedings of the 11th International Conference on Ubiquitous Computing, UbiComp ’09, Orlando, Florida, USA (September 2009), Association for Computing Machinery), 31-40
[60] Shokri, Reza; Papadimitratos, Panos; Theodorakopoulos, George; Hubaux, Jean-Pierre, Collaborative location privacy, (2011 IEEE Eighth International Conference on Mobile Ad-Hoc and Sensor Systems (October 2011)), 500-509
[61] Shokri, Reza; Theodorakopoulos, George; Le Boudec, Jean-Yves; Hubaux, Jean-Pierre, Quantifying location privacy, (2011 IEEE Symposium on Security and Privacy. Proceedings. 2011 IEEE Symposium on Security and Privacy. Proceedings, 22-25 May 2011, Berkeley/Oakland California, USA, Piscataway (May 2011), IEEE), 247-262
[62] Stenneth, Leon; Yu, Phillip S.; Wolfson, Ouri, Mobile systems location privacy: “MobiPriv” a robust k anonymous system, (2010 IEEE 6th International Conference on Wireless and Mobile Computing, Networking and Communications (October 2010)), 54-63
[63] Sun, Gang; Liao, Dan; Li, Hui; Yu, Hongfang; Chang, Victor, L2P2: A location-label based approach for privacy preserving in LBS, Future Gener. Comput. Syst., 74, 375-384 (September 2017)
[64] Wightman, Pedro Mario; Zurbarán, Mayra; Rodríguez, Miguel; Labrador, Miguel A., MaPIR: mapping-based private information retrieval for location privacy in LBISs, (38th Annual IEEE Conference on Local Computer Networks - Workshops (October 2013)), 964-971
[65] Xiao, Yonghui; Xiong, Li; Zhang, Si; Cao, Yang, LocLok: location cloaking with differential privacy via hidden Markov model, Proc. VLDB Endow., 10, 12, 1901-1904 (August 2017)
[66] Xu, Toby; Cai, Ying, Location anonymity in continuous location-based services, (Proceedings of the 15th Annual ACM International Symposium on Advances in Geographic Information Systems. Proceedings of the 15th Annual ACM International Symposium on Advances in Geographic Information Systems, GIS ’07, Seattle, Washington (November 2007), Association for Computing Machinery), 1-8
[67] Xu, Toby; Cai, Ying, Feeling-based location privacy protection for location-based services, (Proceedings of the 16th ACM Conference on Computer and Communications Security. Proceedings of the 16th ACM Conference on Computer and Communications Security, CCS ’09, Chicago, Illinois, USA (2009), ACM Press), 348
[68] Xue, Mingqiang; Kalnis, Panos; Keng Pung. Location, Hung, diversity: enhanced privacy protection in location based services, (Choudhury, Tanzeem; Quigley, Aaron; Strang, Thomas; Suginuma, Koji, Location and Context Awareness. Location and Context Awareness, Lecture Notes in Computer Science (2009), Springer: Springer Berlin, Heidelberg), 70-87
[69] Lung Yiu, Man; Jensen, Christian S.; Huang, Xuegang; Lu, Hua, SpaceTwist: managing the trade-offs among location privacy, query performance, and query accuracy in mobile services, (2008 IEEE 24th International Conference on Data Engineering (April 2008)), 366-375
[70] You, Tun-Hao; Peng, Wen-Chih; Lee, Wang-Chien, Protecting moving trajectories with dummies, (2007 International Conference on Mobile Data Management (May 2007)), 278-282
[71] Yu, Lei; Liu, Ling; Pu, Calton, Dynamic differential location privacy with personalized error bounds, (Proceedings 2017 Network and Distributed System Security Symposium. Proceedings 2017 Network and Distributed System Security Symposium, San Diego, CA (2017), Internet Society)
[72] Zhong, Ge; Goldberg, Ian; Hengartner, Urs, Louis, Lester and Pierre: three protocols for location privacy, (Borisov, Nikita; Golle, Philippe, Privacy Enhancing Technologies. Privacy Enhancing Technologies, Lecture Notes in Computer Science (2007), Springer: Springer Berlin, Heidelberg), 62-76
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.