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 formulae 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 formulae 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We recall that we are using a notion of privacy in which all databases have the same number of records n, and the absence of a record is represented by a special value.
References
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258–273 (2009)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_79
de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3) (2008)
Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Converging from branching to linear metrics on Markov chains. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 349–367. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_21
Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Proceedings of POPL. ACM (2012)
Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Log. Methods Comput. Sci. 10(1) (2014)
Bloom, B., Fokkink, W.J., van Glabbeek, R.J.: Precongruence formats for decorated trace semantics. ACM Trans. Comput. Log. 5(1), 26–78 (2004)
van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005)
Castiglioni, V., Gebler, D., Tini, S.: Logical characterization of bisimulation metrics. In: Proceedings of QAPL’16. EPTCS 227, 44–62 (2016)
Castiglioni, V., Tini, S.: Logical characterization of trace metrics. In: Proceedings of QAPL@ETAPS 2017. EPTCS 250, 39–74 (2017)
Chatzikokolakis, K., Andrés, M.E., Bordenabe, N.E., Palamidessi, C.: Broadening the scope of differential privacy using metrics. In: De Cristofaro, E., Wright, M. (eds.) PETS 2013. LNCS, vol. 7981, pp. 82–102. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39077-7_5
Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 32–46. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_4
Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. Electr. Notes Theor. Comput. Sci. 153(2), 79–96 (2006)
Deng, Y., Du, W.: Logical, metric, and algorithmic characterisations of probabilistic bisimulation. CoRR abs/ arXiv:1103.4577 (2011)
Deng, Y., van Glabbeek, R.J.: Characterising probabilistic processes logically - (extended abstract). In: Proceedings of LPAR-17, pp. 278–293 (2010)
Deng, Y., Palamidessi, C., Pang, J.: Weak probabilistic anonymity. ENTCS 180(1), 55–76 (2007)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)
Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. Proc. LICS 2002, 413–422 (2002)
Du, W., Deng, Y., Gebler, D.: Behavioural pseudometrics for nondeterministic probabilistic systems. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 67–84. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47677-3_5
Duchi, J.C., Jordan, M.I., Wainwright, M.J.: Local privacy and statistical minimax rates. In: Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 429–438. IEEE Computer Society (2013)
Dwork, C.: Differential privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 1–12. Springer, Heidelberg (2006). https://doi.org/10.1007/11787006_1
Erlingsson, Ú., Pihur, V., Korolova, A.: RAPPOR: randomized aggregatable privacy-preserving ordinal response. In: Ahn, G., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 1054–1067. ACM (2014)
Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: POPL, pp. 357–370 (2013)
Ghosh, A., Roughgarden, T., Sundararajan, M.: Universally utility-maximizing privacy mechanisms. In: Proceedings of the 41st Annual ACM Symposium on Theory of Computing (STOC), pp. 351–360. ACM (2009)
Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP Work, Conference on Programming, Concepts and Methods, pp. 443–458 (1990)
Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68(1–3), 125–145 (1986)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512–535 (1994)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32, 137–161 (1985)
Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209(2), 154–172 (2011)
Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)
Kwiatkowska, M., Norman, G.: Probabilistic metric semantics for a simple language with recursion. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 419–430. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61550-4_167
Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: approximate reasoning for Markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681–692. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32589-2_59
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Machanavajjhala, A., Kifer, D., Abowd, J.M., Gehrke, J., Vilhuber, L.: Privacy: theory meets practice on the map. Proc. ICDE 2008, 277–286 (2008)
Narayanan, A., Shmatikov, V.: De-anonymizing social networks. In: Proceedings of S&P 2009, pp. 173–187 (2009)
Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Proceedings of ICFP, pp. 157–168. ACM (2010)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)
Smith, A.D.: Efficient, differentially private point estimators. CoRR abs/ arXiv:0809.4794 (2008)
Song, L., Deng, Y., Cai, X.: Towards automatic measurement of probabilistic processes. Proc. QSIC 2007, 50–59 (2007)
Tschantz, M.C., Kaynar, D., Datta, A.: Formal verification of differential privacy for interactive systems (extended abstract). ENTCS 276, 61–79 (2011)
Xu, L., Chatzikokolakis, K., Lin, H.: Metrics for differential privacy in concurrent systems. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 199–215. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43613-4_13
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Castiglioni, V., Chatzikokolakis, K., Palamidessi, C. (2018). A Logical Characterization of Differential Privacy via Behavioral Metrics. In: Bae, K., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2018. Lecture Notes in Computer Science(), vol 11222. Springer, Cham. https://doi.org/10.1007/978-3-030-02146-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-02146-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02145-0
Online ISBN: 978-3-030-02146-7
eBook Packages: Computer ScienceComputer Science (R0)