Skip to Main content Skip to Navigation
Conference papers

A Logical Characterization of Differential Privacy via Behavioral Metrics

Abstract : Differential privacy is a formal definition of privacy ensuring that sensitive information relative to individuals cannot be inferred by querying a database. In this paper, we exploit a modeling of this framework via labeled Markov Chains (LMCs) to provide a logical characterization of differential privacy: we consider a probabilistic variant of the Hennessy-Milner logic and we define a syntactical distance on for-mulae in it measuring their syntactic disparities. Then, we define a trace distance on LMCs in terms of the syntactic distance between the sets of formulae satisfied by them. We prove that such distance corresponds to the level of privacy of the LMCs. Moreover, we use the distance on for-mulae to define a real-valued semantics for them, from which we obtain a logical characterization of weak anonymity: the level of anonymity is measured in terms of the smallest formula distinguishing the considered LMCs. Then, we focus on bisimulation semantics on nondeterministic probabilistic processes and we provide a logical characterization of generalized bisimulation metrics, namely those defined via the generalized Kantorovich lifting. Our characterization is based on the notion of mimicking formula of a process and the syntactic distance on formulae, where the former captures the observable behavior of the corresponding process and allows us to characterize bisimilarity. We show that the generalized bisimulation distance on processes is equal to the syntactic distance on their mimicking formulae. Moreover, we use the distance on mimicking formulae to obtain bounds on differential privacy.
Complete list of metadatas

Cited literature [41 references]  Display  Hide  Download
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, December 30, 2018 - 1:40:16 AM
Last modification on : Thursday, March 5, 2020 - 6:34:00 PM
Long-term archiving on: : Sunday, March 31, 2019 - 12:44:03 PM


Files produced by the author(s)




Valentina Castiglioni, Konstantinos Chatzikokolakis, Catuscia Palamidessi. A Logical Characterization of Differential Privacy via Behavioral Metrics. Formal Aspects of Component Software (FACS 2018), Oct 2018, Pohang, South Korea. pp.75-96, ⟨10.1007/978-3-030-02146-7_4⟩. ⟨hal-01966870⟩



Record views


Files downloads