Defining Privacy Is Supposed to Be Easy

Sebastian Alexander Mödersheim, Thomas Gross, Luca Viganò

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
PublisherSpringer
Publication date2013
Pages619-635
ISBN (Print)978-3-642-45220-8
ISBN (Electronic)978-3-642-45221-5
DOIs
Publication statusPublished - 2013
Event19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013) - Stellenbosch, South Africa
Duration: 14 Dec 201319 Dec 2013
http://www.lpar-19.info/

Conference

Conference19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013)
CountrySouth Africa
CityStellenbosch
Period14/12/201319/12/2013
Internet address
SeriesLecture Notes in Computer Science
Volume8312
ISSN0302-9743

Fingerprint Dive into the research topics of 'Defining Privacy Is Supposed to Be Easy'. Together they form a unique fingerprint.

Cite this