Kouzapas, Dimitrios and Philippou, Anna - Privacy by typing in the $\pi$-calculus

lmcs:4152 - Logical Methods in Computer Science, December 20, 2017, Volume 13, Issue 4
Privacy by typing in the $\pi$-calculus

Authors: Kouzapas, Dimitrios and Philippou, Anna

In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system stores and manipulates information. We develop a correspondence between the above schema and an associated model of computation. In particular, we propose the \Pcalc, a calculus based on the $\pi$-calculus with groups extended with constructs for reasoning about private data. The privacy requirements of an information system are captured via a privacy policy language. The correspondence between the privacy model and the \Pcalc semantics is established using a type system for the calculus and a satisfiability definition between types and privacy policies. We deploy a type preservation theorem to show that a system respects a policy and it is safe if the typing of the system satisfies the policy. We illustrate our methodology via analysis of two use cases: a privacy-aware scheme for electronic traffic pricing and a privacy-preserving technique for speed-limit enforcement.


Source : oai:arXiv.org:1710.06494
DOI : 10.23638/LMCS-13(4:27)2017
Volume: Volume 13, Issue 4
Published on: December 20, 2017
Submitted on: December 20, 2017
Keywords: Computer Science - Logic in Computer Science,Computer Science - Cryptography and Security


Share

Browsing statistics

This page has been seen 54 times.
This article's PDF has been downloaded 20 times.