一句话：提出带组的π演算扩展Pcalc及类型系统，通过类型与隐私策略的可满足性确保系统遵守策略。
本文关注信息系统中隐私的形式化研究，提出一个两轴框架：一轴将隐私视为权利分类，另一轴刻画信息系统存储与处理信息的方式，并建立该框架与计算模型之间的对应。为此，作者在带组的π演算基础上扩展出Pcalc，加入对私有数据推理的构造；隐私需求由隐私策略语言描述。论文用类型系统和类型与策略之间的可满足性定义连接隐私模型与Pcalc语义，并证明类型保持定理：若系统的类型满足策略，则系统尊重该策略且是安全的。最后通过电子交通定价和限速执法两个用例展示方法。
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. Comment: 43 pages
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1710-06494,
title = {Privacy by typing in the $\pi$-calculus},
author = {Dimitrios Kouzapas and Anna Philippou},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:27)2017}
}