Modular Reasoning about Differential Privacy in a Probabilistic Process Calculus
Résumé
The verification of systems for protecting sensitive and confidential information is becoming an increasingly important issue. Differential privacy is a promising notion of privacy originated from the community of statistical databases, and now widely adopted in various models of computation aiming at the protection of confidential information. We consider a probabilistic process calculus as a specification formalism for concurrent systems, and we establish a framework for reasoning about the degree of differential privacy provided by such systems. We investigate the constructs, specify restricted forms of some particular operators, and prove how they preserve or decrease the degree of privacy under composition. We illustrate our ideas on an anonymity-preservation property for an extension of the Crowds protocol. Finally, we make a first step towards computing the channel matrix and the degree of privacy in a process-algebraic setting.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)