Privacy by typing in the $\pi$-calculus

In this paper we propose a formal framework for studying privacy ininformation systems. The proposal follows a two-axes schema where the firstaxis considers privacy as a taxonomy of rights and the second axis involves theways an information system stores and manipulates information. We develop acorrespondence between the above schema and an associated model of computation.In particular, we propose the \Pcalc, a calculus based on the $\pi$-calculuswith groups extended with constructs for reasoning about private data. Theprivacy requirements of an information system are captured via a privacy policylanguage. The correspondence between the privacy model and the \Pcalc semanticsis established using a type system for the calculus and a satisfiabilitydefinition between types and privacy policies. We deploy a type preservationtheorem to show that a system respects a policy and it is safe if the typing ofthe system satisfies the policy. We illustrate our methodology via analysis oftwo use cases: a privacy-aware scheme for electronic traffic pricing and aprivacy-preserving technique for speed-limit enforcement.Comment: 43 page