Defining privacy is supposed to be easy
Date: April 29, 2016
Time: 11:50 – 12:50
Location: Meeting Room Levico - Polo Scientifico e Tecnologico "Fabio Ferrari" (Edificio Povo 2, via Sommarive 9 – Povo, Trento)
Speaker
Prof. Luca Viganò - King’s College London, UK
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 a novel and declarative way to specify privacy goals, called “alpha‐beta privacy”, and relate it to static equivalence. This new approach is based on specifying two formulae alpha and beta in first‐order logic with Herbrand universes, where alpha reflects the intentionally released information and beta includes the actual cryptographic (“technical”) messages the intruder can see.
Then alpha‐beta privacy means that the intruder cannot derive any “non‐technical” statement from beta that he cannot derive from alpha already. We describe by a variety of examples how this notion can be used in practice. Even though alpha‐beta 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 alpha‐beta privacy.
Joint work with Sebastian Mödersheim and Thomas Groß.
About the speaker
Luca Viganò joined King's College London in October 2013 as a Professor of Computer Science (Software Modelling and Applied Logic). He graduated in Electronic Engineering at the university of his hometown, Genova, Italy, and received his PhD in Computer Science from the University of Saarbruecken, Germany. Before joining King’s, he was a senior research scientist at the University of Freiburg, Germany, and at ETH Zurich, Switzerland, and was appointed Associate Professor at the University of Verona, Italy.
His research focuses on formal methods and tools for the specification, verification, and construction of secure and private systems. On these topics, he has published extensively, coordinated and participated in a large number of research and industrial projects, and taught several courses, tutorials and industrial courses.
Contact person regarding this talk: Fabio Massacci, fabio.massacci [at] unitn.it