An Epistemic Approach to Compositional Reasoning about Anonymity and Privacy
This work addresses foundational issues in privacy verification for system designers, offering incremental theoretical insights into compositional reasoning.
The paper tackles the problem of ensuring privacy properties like anonymity remain valid when systems are composed sequentially or in parallel, showing that compositionality fails without specific independence assumptions and providing theoretical conditions to guarantee it.
In this paper, we present an epistemic logic approach to the compositionality of several privacy-related informationhiding/ disclosure properties. The properties considered here are anonymity, privacy, onymity, and identity. Our initial observation reveals that anonymity and privacy are not necessarily sequentially compositional; this means that even though a system comprising several sequential phases satisfies a certain unlinkability property in each phase, the entire system does not always enjoy a desired unlinkability property. We show that the compositionality can be guaranteed provided that the phases of the system satisfy what we call the independence assumptions. More specifically, we develop a series of theoretical case studies of what assumptions are sufficient to guarantee the sequential compositionality of various degrees of anonymity, privacy, onymity, and/or identity properties. Similar results for parallel composition are also discussed.