Skip to main content

Logical Reasoning About Obligations

Researcher: Frank Pfenning

Research Area: Privacy Protection

Cross Cutting Thrusts: Formal Methods


An important component of privacy policies is that principals performing certain actions incur specific obligations. If we want to formally express privacy policies, we will need to capture the notion of obligation, even if the enforcement of obligations may external in some cases. The short summary of the the proposed work is that we intend to develop, analyze and implement a logic that can capture not only access control but also obligations incurred while accessing certain resources.

In prior work, we have proposed a logical framework for expressing authorization and information flow properties in distributed systems. A fragment of this framework has been used in a system of proof-carrying authorization where access control decisions are based on explicit proofs of compliance with a policy. One important aspect of this system is that it is linear. The logical notion of a linear assumption allows us to support use-once certificates and proofs. A use-once certificate, or a proof based on it, is a capability or permission we can exercise only once. For example, we may have permission to read a file once, to submit a homework solution only once, to spend electronic cash only once, or to enter an office only once. The basic idea of the proposed logical rendering is that an obligation is a negated linear assumption.

In furthering this research, we propose to 1) design an appropriate logical notion of obligation, most likely based on a form of linear negation; 2) develop several small case studies for the use of obligations in the context of privacy policies; 3) implement a prototype to demonstrate specification of obligations and to the extent possible in a given domain, discharge and enforcement of obligations and 4)integrate a notion of time to express policies where obligations have explicit temporal aspects.