Type checking purpose-based privacy policies in the π-calculus

Abstract

In this paper we propose a formal framework for studying privacy preserving policies based on the notion of purpose. Our framework employs the π-calculus with groups accompanied by a type system for capturing privacy requirements. It also incorporates a privacy policy language which captures how different entities within a system, which are distinguished by their roles, may access sensitive information and the purposes for which they are allowed to process the data. We show that a system respects a policy if the typing of the system is compatible with the policy. We illustrate our methodology via analysis of privacy aware services of a health-care system. © Springer International Publishing Switzerland 2016.