A. Aldini, A. Bogliolo, C. Ballester-lafuente, and J. Seigneur, On the Tradeoff among Trust, Privacy, and Cost in Incentive-Based Networks, IFIPTM, volume 430 of IFIP Advances in Information and Communication Technology, pp.205-212
DOI : 10.1007/978-3-662-43813-8_14
URL : https://hal.archives-ouvertes.fr/hal-01381689

[. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.1-70, 1999.
DOI : 10.1145/266420.266432

M. E. Andrés, C. Palamidessi, A. Sokolova, and P. Van-rossum, Information hiding in probabilistic concurrent systems, Theoretical Computer Science, vol.412, issue.28, pp.3072-3089, 2011.
DOI : 10.1016/j.tcs.2011.02.045

M. E. Andrés, C. Palamidessi, G. Peter-van-rossum, and . Smith, Computing the leakage of informationhiding systems, Proc. of TACAS, pp.373-389, 2010.

[. Bacci, G. Bacci, G. Kim, R. Larsen, and . Mardare, Computing Behavioral Distances, Compositionally, Proc. MFCS'13, pp.74-85, 2013.
DOI : 10.1007/978-3-642-40313-2_9

[. Bacci, G. Bacci, K. G. Larsen, and R. Mardare, On-the-Fly Exact Computation of Bisimilarity Distances, TACAS, pp.1-15
DOI : 10.1007/978-3-642-36742-7_1

[. Braun, K. Chatzikokolakis, and C. Palamidessi, Compositional methods for informationhiding, Proc. of FOSSACS, pp.443-457, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01006384

G. Gilles-barthe, B. Danezis, C. Grégoire, S. Z. Kunz, and . Béguelin, Verified computational differential privacy with applications to smart metering, CSF, pp.287-301, 2013.

J. [. Bergstra, B. Klop-gilles-barthe, F. Köpf, S. Z. Olmedo, and . Béguelin, Process algebra for synchronous communication Information and Control Probabilistic relational reasoning for differential privacy, Proc. of POPL, pp.109-137, 1984.

M. Boreale, Quantifying information leakage in process calculi, Automata, Languages and Programming, 33rd Int. Colloquium Proc., Part II, pp.119-131, 2006.

[. Bhargava and C. Palamidessi, Probabilistic Anonymity, Proc. of CONCUR, pp.171-185, 2005.
DOI : 10.1007/11539452_16
URL : https://hal.archives-ouvertes.fr/inria-00201101

E. Bandini and R. Segala, Axiomatizations for Probabilistic Bisimulation, Proc. of ICALP, pp.370-381, 2001.
DOI : 10.1007/3-540-48224-5_31

[. Breugel, B. Sharma, and J. Worrell, Approximating a Behavioural Pseudometric Without Discount for Probabilistic Systems, Foundations of Software Science and Computational Structures, pp.123-137, 2007.
DOI : 10.1007/978-3-540-71389-0_10

W. [. Baeten and . Weijland, Proces algebra, volume 18 of Cambridge tracts in theoretical computer science, 1990.

[. Chatzikokolakis and E. Miguel, Andrés, Nicolás Emilio Bordenabe, and Catuscia Palamidessi. Broadening the scope of differential privacy using metrics

L. Canetti, D. Cheung, M. Kaynar, and . Liskov, Taskstructured probabilistic i/o automata, Proc. of WODES, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00080681

[. Chatterjee, R. Luca-de-alfaro, V. Majumdar, and . Raman, Algorithms for Game Metrics, FSTTCS Leibniz-Zentrum fuer Informatik, pp.107-118, 2008.
DOI : 10.2168/LMCS-6(3:13)2010

[. Cai and Y. Gu, Measuring Anonymity, ISPEC, pp.183-194, 2009.
DOI : 10.1007/3-540-36467-6_9

[. Chatzikokolakis, D. Gebler, C. Palamidessi, and L. Xu, Generalized bisimulation met- Bibliography rics [Cha88] David Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability, Proc. of CONCUR, pp.32-4665, 1988.

S. Cheng, A crash course on the lebesgue integral and measure theory, 2008.

[. Clark, S. Hunt, and P. Malacaria, Quantitative information flow, relations and polymorphic types Bisimulation for demonic schedulers, CNP09] Konstantinon Chatzikokolakis Proc. of FOSSACS, pp.181-199, 2005.

[. Chatzikokolakis and C. Palamidessi, Probable innocence revisited, Theoretical Computer Science, vol.367, issue.1-2, pp.123-138, 2006.
DOI : 10.1016/j.tcs.2006.08.033
URL : https://hal.archives-ouvertes.fr/inria-00201109

[. Chatzikokolakis and C. Palamidessi, Making random choices invisible to the scheduler, Information and Computation, vol.208, issue.6, pp.694-715, 2010.
DOI : 10.1016/j.ic.2009.06.006
URL : https://hal.archives-ouvertes.fr/inria-00424860

G. Comanici and D. Precup, Basis Function Discovery Using Spectral Clustering and Bisimulation Metrics, AAAI, pp.85-99, 2012.
DOI : 10.1007/978-3-642-28499-1_6

[. Chatzikokolakis, C. Palamidessi, and C. Braun, Compositional methods for informationhiding
URL : https://hal.archives-ouvertes.fr/hal-01006384

[. Clarke, O. Sandberg, B. Wiley, and T. W. Hong, Freenet: A Distributed Anonymous Information Storage and Retrieval System, Proc. of DIAU, pp.44-66, 2000.
DOI : 10.1007/3-540-44702-4_4

M. Thomas, J. A. Cover, and . Thomas, Elements of Information Theory, 1991.

D. Chen, F. Van-breugel, and J. Worrell, On the Complexity of Computing Probabilistic Bisimilarity, FOSSACS, pp.437-451, 2012.
DOI : 10.1007/978-3-642-28729-9_29

A. Das, N. Borisov, P. Mittal, and M. Caesar, Re 3 : relay reliability reputation for anonymity systems, ASIACCS, pp.63-74, 2014.

[. Deng and W. Du, The Kantorovich Metric in Computer Science: A Brief Survey, Electronic Notes in Theoretical Computer Science, vol.253, issue.3, pp.73-82, 2009.
DOI : 10.1016/j.entcs.2009.10.006

F. David-de-frutos-escrig, C. Rosa-velardo, and . Gregorio-rodríguez, New Bisimulation Semantics for Distributed Systems, In FORTE, vol.360, issue.1-3, pp.143-159, 2007.
DOI : 10.1016/j.tcs.2006.03.004

R. D. Pedro, D. Argenio, M. D. Gebler, and . Lee, Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules, Proc. of FoSSaCS, pp.289-303, 2014.

[. Deng and M. Hennessy, Compositional reasoning for weighted Markov decision processes, Science of Computer Programming, vol.78, issue.12, pp.2537-2579, 2013.
DOI : 10.1016/j.scico.2013.02.009

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, The metric analogue of weak bisimulation for probabilistic processes, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.413-422, 2002.
DOI : 10.1109/LICS.2002.1029849

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, Metrics for labelled Markov processes, Theoretical Computer Science, vol.318, issue.3, pp.323-354, 2004.
DOI : 10.1016/j.tcs.2003.09.013

C. Dwork, K. Kenthapadi, F. Mcsherry, I. Mironov, and M. Naor, Our Data, Ourselves: Privacy Via Distributed Noise Generation, EUROCRYPT, pp.486-503, 2006.
DOI : 10.1007/11761679_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.3527

C. Dwork and J. Lei, Differential privacy and robust statistics, Proceedings of the 41st annual ACM symposium on Symposium on theory of computing, STOC '09, pp.371-380, 2009.
DOI : 10.1145/1536414.1536466

J. Desharnais, F. Laviolette, and M. Tracol, Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.264-273, 2008.
DOI : 10.1109/QEST.2008.42

. Tor, The second-generation onion router, Proc. of the 13th USENIX Security Symposium, 2004.

Y. Deng and C. Palamidessi, Axiomatizations for probabilistic finite-state behaviors, Proc. of FOSSACS, pp.110-124, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00159682

[. Deng, C. Palamidessi, and J. Pang, Compositional Reasoning for Probabilistic Finite-State Behaviors, Processes, Terms and Cycles: Steps on the Road to Infinity, pp.309-337, 2005.
DOI : 10.1007/11601548_17
URL : https://hal.archives-ouvertes.fr/hal-00159683

[. Deng, C. Palamidessi, and J. Pang, Weak Probabilistic Anonymity, Proc. of the 3rd Int. Workshop on Security Issues in Concurrency (SecCo), pp.55-76, 2007.
DOI : 10.1016/j.entcs.2005.05.047
URL : https://hal.archives-ouvertes.fr/hal-00159688

[. Deng, J. Pang, and P. Wu, Measuring Anonymity with Relative Entropy, Proc. of the 4th Int. Worshop on Formal Aspects in Security and Trust, pp.65-79, 2006.
DOI : 10.1007/978-3-540-75227-1_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.78.1531

[. Dwork, Differential Privacy, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Proceedings, Part II, pp.1-12, 2006.
DOI : 10.1007/11787006_1

[. Dwork, A firm foundation for private data analysis, Communications of the ACM, vol.54, issue.1, pp.86-96, 2011.
DOI : 10.1145/1866739.1866758

R. Focardi and R. Gorrieri, Classification of security properties (part i: Information flow), FOSAD, pp.331-396, 2000.

M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce, Linear dependent types for differential privacy, POPL, pp.357-370, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909340

M. Hennessy, A calculus for costed computations, Logical Methods in Computer Science, vol.7, issue.1, 2011.
DOI : 10.2168/LMCS-7(1:7)2011

[. Hansson and B. Jonsson, A calculus for communicating systems with time and probabitilies, Proceedings of the Real-Time Systems Symposium -1990, pp.278-287, 1990.

[. Hennessy and H. Lin, Proof systems for message-passing process algebras, In CONCUR LNCS, vol.715, pp.202-216, 1993.

Y. Joseph, K. R. Halpern, and . Neill, Anonymity and information hiding in multiagent systems, J. of Comp. Security, vol.13, issue.3, pp.483-512, 2005.

]. C. Hoa85 and . Hoare, Communicating Sequential Processes, 1985.

[. Hamadou, C. Palamidessi, V. Sassone, and E. Elsalamouny, Probable innocence in the presence of independent knowledge Workshop on Formal Aspects in Security and Trust Lira: Lightweight incentivized routing for anonymity, Postproceedings of the 6th Int NDSS, pp.141-156, 2010.

C. Jou and S. A. Smolka, Equivalences, congruences, and complete axiomatizations for probabilistic processes, Proc. of CONCUR, pp.367-383, 1990.
DOI : 10.1007/BFb0039071

A. Kiehn and S. Arun-kumar, Amortised Bisimulations, FORTE, pp.320-334, 2005.
DOI : 10.1007/3-540-10235-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.6835

[. Lahaie, How to take the dual of a linear program, 2008.

H. Lin and . Pam, A process algebra manipulator. Formal Methods in System Design, pp.243-259, 1995.

G. Kim, A. Larsen, and . Skou, Bisimulation through probabilistic testing, Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL), pp.344-352, 1989.

G. Kim, A. Larsen, and . Skou, Bisimulation through probabilistic testing, Inf. and Comp, vol.94, issue.1, pp.1-28, 1991.

[. Lin and W. Yi, A Proof System for Timed Automata, FoSSaCS, pp.208-222
DOI : 10.1007/3-540-46432-8_14

P. Malacaria, Assessing security threats of looping constructs [McS09] Frank McSherry. Privacy integrated queries: an extensible platform for privacy-preserving data analysis, Proc. of POPL Proc. of the ACM SIGMOD Int. Conf. on Management of Data, pp.225-235, 2007.

D. Mka-+-08-]-ashwin-machanavajjhala, J. M. Kifer, J. Abowd, L. Gehrke, and . Vilhuber, Privacy: Theory meets practice on the map, Proc. of ICDE, pp.277-286, 2008.

[. Mu, Measuring Information Flow in Reactive Processes, ICICS, pp.211-225, 2009.
DOI : 10.1007/978-3-642-11145-7_17

R. Tsuen-wan-ngan, D. S. Dingledine, and . Wallach, Building Incentives into Tor, Lecture Notes in Computer Science, vol.6052, pp.238-256, 2010.
DOI : 10.1007/978-3-642-14577-3_19

[. Norfolk, When does a metric generate convex balls? Technical report, 1991.

A. Narayanan and V. Shmatikov, De-anonymizing Social Networks, 2009 30th IEEE Symposium on Security and Privacy, pp.173-187, 2009.
DOI : 10.1109/SP.2009.22
URL : http://arxiv.org/abs/0903.3276

J. Reed and B. C. Pierce, Distance makes the types grow stronger: a calculus for differential privacy, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming (ICFP), pp.157-168, 2010.

K. Michael, A. D. Reiter, and . Rubin, Crowds: anonymity for Web transactions, ACM Trans. on Information and System Security, vol.1, issue.1, pp.66-92, 1998.

Y. A. Peter, S. A. Ryan, and . Schneider, Process algebra and non-interference, Journal of Computer Security, vol.9, issue.12, pp.75-103, 2001.

. Roy, T. V. Srinath, A. Setty, V. Kilzer, E. Shmatikov et al., Airavat: security and privacy for MapReduce, Proc. of the 7th USENIX Symposium on Networked Systems Design and Implementation (NSDI), pp.297-312, 2010.

[. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, 1995.

[. Sassone, E. Elsalamouny, and S. Hamadou, Trust in Crowds: Probabilistic Behaviour in Anonymity Protocols, Proc. of the Fifth Int. Symposium on Trustworthly Global Computing, pp.88-102, 2010.
DOI : 10.1007/978-3-642-15640-3_7

F. Paul, D. M. Syverson, M. G. Goldschlag, and . Reed, Anonymous connections and onion routing, Proc. of S&P, pp.44-54, 1997.

[. Sassone, S. Hamadou, and M. Yang, Trust in Anonymity Networks, Proceedings of CONCUR, pp.48-70, 1994.
DOI : 10.1007/978-3-642-15375-4_5
URL : https://hal.archives-ouvertes.fr/hal-00760437

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, vol.2, issue.2, pp.250-273, 1995.

[. Smith, Probabilistic noninterference through weak probabilistic bisimulation, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., pp.3-13, 2003.
DOI : 10.1109/CSFW.2003.1212701
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.7841

A. Smith, Efficient, differentially private point estimators . arXiv preprint, 2008.

[. Smith, On the Foundations of Quantitative Information Flow, Proc. of FOSSACS, pp.288-302, 2009.
DOI : 10.1137/060651380

A. Sokolova and E. P. De-vink, Probabilistic Automata: System Types, Parallel Composition and Comparison, Validation of Stochastic Systems: A Guide to Current Research, pp.1-43, 2004.
DOI : 10.1007/978-3-540-24611-4_1

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

[. Tracol, J. Desharnais, and A. Zhioua, Computing Distances between Probabilistic Automata, QAPL, pp.148-162, 2011.
DOI : 10.4204/EPTCS.57.11
URL : http://doi.org/10.4204/eptcs.57.11

E. [. Thorsley and . Klavins, Approximating stochastic biochemical processes with Wasserstein pseudometrics, IET Systems Biology, vol.4, issue.3, pp.193-211, 2010.
DOI : 10.1049/iet-syb.2009.0039

C. Michael, D. Tschantz, A. Kaynar, and . Datta, Formal verification of differential privacy for interactive systems (extended abstract), Electron. Notes Theor. Comput. Sci, vol.276, pp.61-79, 2011.

J. Franck-van-breugel and . Worrell, An Algorithm for Quantitative Verification of Probabilistic Transition Systems
DOI : 10.1007/3-540-44685-0_23

F. Van-breugel and J. Worrell, Towards quantitative verification of probabilistic transition systems [vBW05] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems, Proc. of CONCUR'01 Proc. of ICALP, pp.336-350, 2001.

R. J. Van-glabbeek, S. A. Smolka, and B. Steffen, Reactive, generative, and stratified models of probabilistic processes, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.59-80, 1995.
DOI : 10.1109/LICS.1990.113740

L. Xu, K. Chatzikokolakis, and H. Lin, Metrics for Differential Privacy in Concurrent Systems, Proc. of FORTE, pp.199-215
DOI : 10.1007/978-3-662-43613-4_13
URL : https://hal.archives-ouvertes.fr/hal-00879140

L. Xu, S. Hamadou, and C. Palamidessi, Privacy-preserving process constructors, 2014.

L. Xu and H. Lin, Complete Proof Systems for Amortised Probabilistic Bisimulations, Journal of Computer Science and Technology, vol.2, issue.2, 2014.
DOI : 10.1007/s11390-016-1628-4

L. Xu, Modular Reasoning about Differential Privacy in a Probabilistic Process Calculus, TGC, pp.198-212, 2012.
DOI : 10.1007/978-3-642-41157-1_13
URL : https://hal.archives-ouvertes.fr/hal-00691284

[. Yang, V. Sassone, and S. Hamadou, A Game-Theoretic Analysis of Cooperation in Anonymity Networks
DOI : 10.1007/978-3-642-28641-4_15
URL : https://hal.archives-ouvertes.fr/hal-00760445