Skip to main content

Privacy, Information Disclosure, & Authorization from a Logical Perspective

Researchers: Frank Pfenning, Lujo Bauer

Abstract

Privacy, Information Disclosure, and Authorization from a Logical Perspective

What is privacy? Once we have a definition, how do we enforce adherence to privacy policies? And, finally, how do we circumscribe the consequences of policy definitions in a rigorous manner?

These questions are the subject of much current research, but we are still far away from a grand unifying theory of privacy and information flow. One of the problems is that these questions have many social and psychological components that are difficult to reconcile with their mathematical and computational aspects. Yet even on the foundational side our understanding of privacy and limited information disclosure is still highly incomplete, despite recent advances.

We propose to investigate the above questions from a logical perspective. More precisely, we propose to develop logical concepts through which reasoning with privacy can be made rigorous. Privacy policies can be expressed as axioms or theories within an underlying logic. Policies can be enforced and explained via proofs. For example, we may grant limited access to a piece of data because we are presented with a proof object establishing that this form of access does not violate a given privacy policy. Finally, we may formally reason about a policy by exploiting the intrinsic structure of logical proofs.

The logical approach has several advantages over current attempts that are more operational in flavor. Perhaps most importantly, logic is endowed with an internal notion of justification, namely proof. This provides the link between policy specification, policy enforcement, and reasoning about policies in a scalable and flexible way. Secondly, modern logical systems are constructed in an inherently open-ended way, which means that we can add and subtract logical operators to respond to the demands of the application in a modular way. It also allows both developers and users to understand the logical connectives largely independently instead of as complex web of tightly interconnected pieces.