M. Abadi and C. Fournet, Private authentication, Theoretical Computer Science, vol.322, issue.3, pp.427-476, 2004.
DOI : 10.1016/j.tcs.2003.12.023

M. 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. Roberto, D. Amadio, and . Lugiez, On the reachability problem in cryptographic protocols, Proceedings of CONCUR 00, 2000.

R. Beauxis, K. Chatzikokolakis, C. Palamidessi, and P. Panangaden, Formal Approaches to Information-Hiding (Tutorial), Proceedings of the Third Symposium on Trustworthy Global Computing, pp.347-362, 2007.
DOI : 10.1007/978-3-540-78663-4_23
URL : https://hal.archives-ouvertes.fr/inria-00261827

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

M. Boreale and D. Sangiorgi, Some congruence properties for ??-calculus bisimilarities, Theoretical Computer Science, vol.198, issue.1-2, pp.159-176, 1998.
DOI : 10.1016/S0304-3975(97)00125-4
URL : https://hal.archives-ouvertes.fr/inria-00073821

K. Chatzikokolakis, G. Norman, and D. Parker, Bisimulation for Demonic Schedulers, Proceedings of the Twelfth International Conference on Foundations of Software Science and Computation Structures, 2009.
DOI : 10.1007/3-540-61770-1_38

K. Chatzikokolakis and C. Palamidessi, Making Random Choices Invisible to the Scheduler, Proceedings of CONCUR'07, pp.42-58
DOI : 10.1007/978-3-540-74407-8_4
URL : https://hal.archives-ouvertes.fr/inria-00424860

K. Chatzikokolakis, C. Palamidessi, and P. Panangaden, Anonymity protocols as noisy channels Information and Computation, pp.378-401, 2008.

K. Chatzikokolakis, C. Palamidessi, and P. Panangaden, On the Bayes risk in information-hiding protocols, Journal of Computer Security, vol.16, issue.5, pp.531-571, 2008.
DOI : 10.3233/JCS-2008-0333
URL : https://hal.archives-ouvertes.fr/inria-00349224

D. Chaum, The dining cryptographers problem: Unconditional sender and recipient untraceability, Journal of Cryptology, vol.1, issue.1, pp.65-75, 1988.
DOI : 10.1007/BF00206326

I. Clarke, O. Sandberg, B. Wiley, and T. W. Hong, Freenet: A Distributed Anonymous Information Storage and Retrieval System, Designing Privacy Enhancing Technologies , International Workshop on Design Issues in Anonymity and Unobservability, pp.44-66, 2000.
DOI : 10.1007/3-540-44702-4_4

C. Díaz, S. Seys, J. Claessens, and B. Preneel, Towards Measuring Anonymity, Proceedings of the workshop on Privacy Enhancing Technologies (PET) 2002, pp.54-68, 2002.
DOI : 10.1007/3-540-36467-6_5

R. D. Gill, M. Van-der-laan, and J. Robins, Coarsening at Random, Proceedings of the First Seattle Symposium in Biostatistics, pp.255-294, 1997.
DOI : 10.1007/978-1-4684-6316-3_14

P. D. Grunwald and J. Y. Halpern, Updating probabilities, Journal of Artificial Intelligence Research, vol.19, pp.243-278, 2003.

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

O. Mihaela, H. , and C. Palamidessi, Probabilistic asynchronous ?-calculus, Proceedings of FOSSACS 2000, pp.146-160, 2000.

C. A. Hoare, Communicating Sequential Processes, 1985.

D. Hughes and V. Shmatikov, Information hiding, anonymity and privacy: a modular approach, Journal of Computer Security, vol.12, issue.1, pp.3-36, 2004.
DOI : 10.3233/JCS-2004-12102

S. Kremer and M. D. Ryan, Analysis of an Electronic Voting Protocol in the Applied Pi Calculus, Programming Languages and Systems ? Proceedings of the 14th European Symposium on Programming, pp.186-200, 2005.
DOI : 10.1007/978-3-540-31987-0_14

G. Lowe and . Casper, Casper: A compiler for the analysis of security protocols, Proceedings of 10th IEEE Computer Security Foundations Workshop, pp.53-84, 1997.
DOI : 10.3233/JCS-1998-61-204

P. Malacaria, Assessing security threats of looping constructs, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.225-235, 2007.

P. Malacaria and H. Chen, Lagrange multipliers and maximum information leakage in different observational models, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security , PLAS '08, pp.135-146, 2008.
DOI : 10.1145/1375696.1375713

R. Milner, Communication and Concurrency. International Series in Computer Science, 1989.

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I and II. Information and Computation A preliminary version appeared as Technical Reports ECF-LFCS-89-85 and -86, pp.1-40, 1989.

C. Palamidessi, Comparing the expressive power of the synchronous and the asynchronous ??-calculus, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.256-265, 1997.
DOI : 10.1145/263699.263731

C. Palamidessi and O. M. Herescu, A Randomized Distributed Encoding of the ??-Calculus with Mixed Choice, Theoretical Computer Science, vol.335, issue.2-3, pp.373-404, 2005.
DOI : 10.1007/978-0-387-35608-2_44

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

A. W. Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, Proceedings The Eighth IEEE Computer Security Foundations Workshop, pp.98-107, 1995.
DOI : 10.1109/CSFW.1995.518556

Y. Peter, S. Ryan, and . Schneider, Modelling and Analysis of Security Protocols, 2001.

D. Sangiorgi, ??-Calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, vol.167, issue.1-2, pp.235-274, 1996.
DOI : 10.1016/0304-3975(96)00075-8

S. Schneider, Security properties and CSP, Proceedings 1996 IEEE Symposium on Security and Privacy, 1996.
DOI : 10.1109/SECPRI.1996.502680

S. Schneider and A. Sidiropoulos, CSP and anonymity, Proc. of the European Symposium on Research in Computer Security (ESORICS), pp.198-218, 1996.
DOI : 10.1007/3-540-61770-1_38

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes An extended abstract, Proceedings of CONCUR '94, pp.250-273, 1995.

A. Serjantov and G. Danezis, Towards an Information Theoretic Metric for Anonymity, Proceedings of the workshop on Privacy Enhancing Technologies (PET) 2002, pp.41-53, 2002.
DOI : 10.1007/3-540-36467-6_4

G. Smith, On the Foundations of Quantitative Information Flow, Proceedings of the Twelfth International Conference on Foundations of Software Science and Computation Structures, pp.288-302, 2009.
DOI : 10.1137/060651380

F. Paul, S. G. Syverson, and . Stubblebine, Group principals and the formalization of anonymity, World Congress on Formal Methods, pp.814-833, 1999.

P. F. Syverson, D. M. Goldschlag, and M. G. Reed, Anonymous connections and onion routing, Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pp.44-54, 1997.
DOI : 10.1109/SECPRI.1997.601314

A. Appendix and A. , 1 The ?-calculus We recall here the basic notions about the ?-calculus. We choose the variant used in [6, 31], which differs from the standard one because is has a guarded choice instead of the free choice. This is convenient because it will allow to introduce the probabilistic ?-calculus, in the next section, in a smoother way. Let N be a countable set of names, x, y The set of prefixes, and the set of ?-calculus processes, P, Q, . . ., are defined by the following abstract syntax