Abstract
Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce in this paper a novel and declarative way to specify privacy goals, called α-β privacy, and relate it to static equivalence. This new approach is based on specifying two formulae α and β in first-order logic with Herbrand universes, where α reflects the intentionally released information and β includes the actual cryptographic (“technical”) messages the intruder can see. Then α-β privacy means that the intruder cannot derive any “non-technical” statement from β that he cannot derive from α already. We describe by a variety of examples how this notion can be used in practice. Even though α-β privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and obtain partial tool support for α-β privacy.
This work was partially supported by the EU FP7 Projects no. 318424, “FutureID: Shaping the Future of Electronic Identity” (futureid.eu), and no. 257876, “SPa- CIoS: Secure Provision and Consumption in the Internet of Services” (spacios.eu) and the PRIN 2010-11 project “Security Horizons”. Much of this work was carried out while L. Viganò was at Dipartimento di Informatica, Università di Verona, Italy
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
Abadi, M.: Private authentication. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol. 2482, pp. 27–40. Springer, Heidelberg (2003)
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under (many more) equational theories. In: CSFW, pp. 62–76. IEEE CS (2005)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104–115. ACM Press (2001)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96. IEEE CS (2001)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. JLAP 75(1), 3–51 (2008)
Cortier, V., Rusinowitch, M., Zalinescu, E.: Relating two standard notions of secrecy. Logical Methods in Computer Science 3(3) (2007)
Delaune, S., Ryan, M., Smyth, B.: Automatic verification of privacy properties in the applied pi-calculus. In: Karabulut, Y., Mitchell, J., Herrmann, P., Jensen, C.D. (eds.) Trust Management II. IFIP, vol. 263, pp. 263–278. Springer, Boston (2008)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Dwork, C.: Differential Privacy: A Survey of Results. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 1–19. Springer, Heidelberg (2008)
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical logic. Springer (1994)
Goubault-Larrecq, J.: Finite models for formal security proofs. J. Comput. Secur. 18(6), 1247–1299 (2010)
Hinrichs, T., Genesereth, M.: Herbrand logic. Technical Report LG-2006-02, Stanford Univ., USA (2006), http://logic.stanford.edu/reports/LG-2006-02.pdf
IBM Research – Zurich. Specification of the identity mixer cryptographic library. version 2.3.4. Technical report, IBM Research (2012)
Mödersheim, S., Groß, T., Viganò, L.: Defining Privacy is Supposed to be Easy (Extended Version). Technical Report 2013-21, DTU Compute, Denmark (2013)
Ryan, P., Schneider, S.: Process algebra and non-interference. In: CSFW. IEEE CS (1999)
Selinger, P.: Models for an Adversary-Centric Protocol Logic. ENTCS 55 (2003)
Sweeney, L.: k-anonymity: A model for protecting privacy. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems 10(5), 557–570 (2002)
Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
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
Mödersheim, S.A., Groß, T., Viganò, L. (2013). Defining Privacy Is Supposed to Be Easy. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_41
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)