Type Checking Privacy Policies in the π-calculus

In this paper we propose a formal framework for studying privacy. Our framework is based on the π-calculus with groups accompanied by a type system for capturing privacy-related notions. The typing system we propose combines a number of concepts from the literature: it includes the use of groups to enable reasoning about information collection, it builds on read/write capabilities to control information processing, and it employs type linearity to restrict information dissemination. Furthermore, we associate our framework with a privacy policy language and we prove that if a system is well-typed according to a typing that is compatible with a policy then the system respects the policy