Abstract
More and more personal information is exchanged on-line using communication protocols. This makes it increasingly important that such protocols satisfy privacy by data minimisation. Formal methods have been used to verify privacy properties of protocols; but so far, mostly in an ad-hoc way. In previous work, we provided general definitions for the fundamental privacy concepts of linkability and detectability. However, this approach is only able to verify privacy properties for given protocol instances. In this work, by generalising the approach, we formally analyse privacy of communication protocols independently from any instance. We implement the model; identify its assumptions by relating it to the instantiated model; and show how to visualise results. To demonstrate our approach, we analyse privacy in Identity Mixer.
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.
Download to read the full chapter text
Chapter PDF
References
Bangerter, E., Camenisch, J., Lysyanskaya, A.: A Cryptographic Framework for the Controlled Release of Certified Data. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2004. LNCS, vol. 3957, pp. 20–42. Springer, Heidelberg (2006)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008)
Butin, D., Bella, G.: Verifying Privacy by Little Interaction and No Process Equivalence. In: Proceedings of SECRYPT 2012. INSTICC Press (2012) (in press)
Camenisch, J., Sommer, D., Zimmermann, R.: A General Certification Framework with Applications to Privacy-Enhancing Certificate Infrastructures. In: Proceedings of SEC 2006. Springer (2006)
Clarke, E.M., Jha, S., Marrero, W.R.: Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols. In: Proceedings of PROCOMET 1998. Chapman & Hall, Ltd. (1998)
Dahl, M., Delaune, S., Steel, G.: Formal Analysis of Privacy for Anonymous Location Based Services. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 98–112. Springer, Heidelberg (2012)
Dong, N., Jonker, H., Pang, J.: Formal Analysis of Privacy in an eHealth Protocol. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 325–342. Springer, Heidelberg (2012)
Dreier, J., Lafourcade, P., Lakhnech, Y.: A Formal Taxonomy of Privacy in Voting Protocols. Tech. report, Verimag (2011)
Hansen, M., Berlich, P., Camenisch, J., Clauß, S., Pfitzmann, A., Waidner, M.: Privacy-Enhancing Identity Management. Inf. Secur. Tech. Rep. 9(1), 35–44 (2004)
Hoepman, J.-H., Joosten, R., Siljee, J.: Comparing Identity Management Frameworks in a Business Context. In: Matyáš, V., Fischer-Hübner, S., Cvrček, D., Švenda, P. (eds.) The Future of Identity. IFIP AICT, vol. 298, pp. 184–196. Springer, Heidelberg (2009)
Identity Management Systems (IMS): Identification and Comparison Study: Independent Centre for Privacy Protection Schleswig-Holstein (2003)
Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Sel. Areas Commun. 21(1), 44–54 (2003)
Data protection guidelines on research in the health sector. Office of the Data Protection Commissioner of Ireland (2007)
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Comput. Secur. 6(1-2), 85–128 (1998)
2011 Cost of Data Breach Study: Global: Ponemon Institute (2011)
Tinabo, R., Mtenzi, F., O’Shea, B.: Anonymisation vs. Pseudonymisation: Which one is most useful for both privacy protection and usefulness of e-healthcare data. In: Proceedings of ICITST 2009. IEEE (2009)
Prescription drug data: HHS has issued health privacy and security regulations but needs to improve guidance and oversight: U.S. Govt. Accountability Office (2012)
Veeningen, M., de Weger, B., Zannone, N.: Formal Modelling of (De)Pseudonymisation: A Case Study in Health Care Privacy. In: Proceedings of STM 2012. Springer (2012)
Veeningen, M., de Weger, B., Zannone, N.: A Formal Privacy Analysis of Identity Management Systems. Tech. report, ArXiv.org (2012)
Veeningen, M., de Weger, B., Zannone, N.: Formal Privacy Analysis of Communication Protocols for Identity Management. In: Jajodia, S., Mazumdar, C. (eds.) ICISS 2011. LNCS, vol. 7093, pp. 235–249. Springer, Heidelberg (2011)
Veeningen, M.: Symbolic Analysis of Identity Mixer. Tech. report (2013), http://www.mobiman.me
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Veeningen, M., de Weger, B., Zannone, N. (2013). Symbolic Privacy Analysis through Linkability and Detectability. In: Fernández-Gago, C., Martinelli, F., Pearson, S., Agudo, I. (eds) Trust Management VII. IFIPTM 2013. IFIP Advances in Information and Communication Technology, vol 401. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38323-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-38323-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38322-9
Online ISBN: 978-3-642-38323-6
eBook Packages: Computer ScienceComputer Science (R0)