Design and Analysis of Privacy Policies.

Organizations, such as hospitals and financial institutions, that use privacy-sensitive information face the challenge of complying with privacy regulations and their own privacy policies. These regulations and policies are often written in natural language (or legalese), making it difficult for information systems to aid in assuring compliance. In this thesis, we propose a formal language for expressing and reasoning about privacy regulations and policies. Other researchers have proposed other privacy languages, but these languages suffer semantic anomalies due to their handling of the "data hierarchy," the relation between different attributes about the same individual. We analyze a number of examples of such anomalies in the Platform for Privacy Preferences and in the Enterprise Privacy Authorization Language and lay out a set of criteria for evaluating privacy languages. We present our language, the Logic of Privacy and Utility, which is based on Contextual Integrity, a theory of privacy expectations from the literatures on law and public policy. Our language formalizes a portion of Contextual Integrity as a concurrent game structure of communicating agents. We then use a fragment of the Alternating-time Temporal Logic of this model as our privacy language and identify specific syntactic forms for expressing the norms of Contextual Integrity. We evaluate the privacy features of the language in three ways. First, we present theorems about the complexity of combination and compliance, distinguishing between weak compliance (which does not consider the feasibility of future obligations) and strong compliance (which guarantees that agents can discharge their future obligations). Second, we compare the language with other approaches to codifying privacy policies, finding that our language generalizes a number of other approaches. Third, we show that the language is capable of expressing the privacy requirements from a number of privacy regulations, including the Health Insurance Portability and Accountability Act. To evaluate the utility features, those features that aid in reasoning about the usefulness of various data practices, we offer a theory of organizational workflows, also known as business processes. In this setting, we examine the trade-offs between privacy and utility in workflow design (including notions of "minimum necessary" information disclosure) and offer practical algorithms for auditing workflow execution to discover agents who both violate their workflow responsibilities and cause the organization to violate its privacy policy.