.. Toward-an-automatic-probabilistic-checker, 139 in the first part, and greatly optimized, according to the results in the second part. List of Figures 1.1 Confluence with ?, Equivalent graphs that are not homeomorphic. . . . . . . . . . . 27

R. M. Amadio, I. Castellani, and D. Sangiorgi, On bisimulations for the asynchronous ??-calculus, An extended abstract appeared in Proceedings of CONCUR '96, pp.291-324, 1998.
DOI : 10.1016/S0304-3975(97)00223-5
URL : https://hal.archives-ouvertes.fr/inria-00073784

[. 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.

A. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

[. 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

[. Beauxis, A smooth probabilistic extension of concurrent constraint programming, Lecture Notes in Computer Science, vol.5404, 2009.

C. [. Brookes, A. W. Hoare, and . Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM, vol.31, issue.3, pp.560-599, 1984.
DOI : 10.1145/828.833

J. A. Bergstra and J. W. Klop, Process algebra for synchronous communication, Information and Control, vol.60, issue.1-3, pp.109-137, 1984.
DOI : 10.1016/S0019-9958(84)80025-X

J. [. Bergstra, J. V. Klop, and . Tucker, Process algebra with asynchronous communication mechanisms, Proceedings of the Seminar on Concurrency, pp.76-95, 1984.
DOI : 10.1007/3-540-15670-4_4

[. Boudol, Asynchrony and the ?-calculus (note) Rapport de Recherche 1702, 1992.

[. Bhargava and C. Palamidessi, Probabilistic Anonymity, Proceedings of CONCURpdf. [BP09] Romain Beauxis and Catuscia Palamidessi. Probabilistic and nondeterministic aspects of anonymity, pp.171-185, 2005.
DOI : 10.1007/11539452_16
URL : https://hal.archives-ouvertes.fr/inria-00201101

[. Beauxis, C. Palamidessi, and F. D. Valencia, On the asynchronous nature of the asynchronous pi-calculus, Concurrency , Graphs and Models, pp.473-492, 2008.

[. Cardelli and A. D. Gordon, Mobile ambients, Theoretical Computer Science, vol.240, issue.1, pp.177-213, 2000.
DOI : 10.1016/S0304-3975(99)00231-5
URL : http://doi.org/10.1016/s0304-3975(99)00231-5

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

[. Chatzikokolakis, C. Palamidessi, and P. Panangaden, Anonymity protocols as noisy channels, TGC, pp.281-300, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00201110

[. 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

]. F. De-boer, J. W. Klop, and C. Palamidessi, Asynchronous communication in process algebra, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.137-147, 1992.
DOI : 10.1109/LICS.1992.185528

J. Engelfriet and T. Gelsema, Multisets and structural congruence of the pi-calculus with replication, Theoretical Computer Science, vol.211, issue.1-2, pp.311-337, 1999.
DOI : 10.1016/S0304-3975(97)00179-5

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

[. Gupta, R. Jagadeesan, and P. Panangaden, Stochastic processes as concurrent constraint programs, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.189-202, 1999.
DOI : 10.1145/292540.292558

[. Gupta, R. Jagadeesan, and V. Saraswat, Probabilistic concurrent constraint programming, CONCUR '97: Concurrency Theory , 8th International Conference, pp.243-257, 1997.
DOI : 10.1007/3-540-63141-0_17

]. R. Gvdlr97, M. Gill, J. Van-der-laan, and . Robins, Coarsening at random: Characterizations, conjectures and counterexamples, Proceedings of the First Seattle Symposium in Biostatistics, Lecture Notes in Statistics, pp.255-294, 1997.

Y. Joseph, K. R. Halpern, and . Neill, Anonymity and information hiding in multiagent systems, Proc. of the 16th IEEE Computer Security Foundations Workshop, pp.75-88, 2003.

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

[. Herescu and C. Palamidessi, Probabilistic Asynchronous ??-Calculus, Proceedings of FOSSACS 2000, pp.146-160, 2000.
DOI : 10.1007/3-540-46432-8_10

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

K. Honda and M. Tokoro, An object calculus for asynchronous communication, Proceedings of the European Conference on Object-Oriented Programming Probabilistic non-determinism, pp.133-147, 1990.
DOI : 10.1007/BFb0057019

[. Kozen, Semantics of probabilistic programs, 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pp.328-350, 1981.
DOI : 10.1109/SFCS.1979.38

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

[. Lynch, Distributed Algorithms, 1996.

[. Milner, A Calculus of Communicating Systems, LNCS, vol.92, 1980.
DOI : 10.1007/3-540-10235-3

]. R. Mil89 and . 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.

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, Lecture Notes in Computer Science, vol.4646, pp.405-419, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

U. Nestmann, What is a ???Good??? Encoding of Guarded Choice?, An extended abstract appeared in the Proceedings of EXPRESS'97, pp.287-319, 2000.
DOI : 10.1006/inco.1999.2822

U. Nestmann and B. C. Pierce, Decoding Choice Encodings, Information and Computation, vol.163, issue.1, pp.1-59, 2000.
DOI : 10.1006/inco.2000.2868

[. 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

[. Palamidessi, A short version of this paper appeared in POPL'97. http://www.lix. polytechnique.fr/ ~ catuscia/papers/pi_calc/mscs.pdf. [PH05a] Catuscia Palamidessi and Oltea M. Herescu. A randomized encoding of the ?-calculus with mixed choice, pdf. [PH05b] Catuscia Palamidessi and Oltea Mihaela Herescu. A randomized encoding of the pi-calculus with mixed choice, pp.685-719373, 2003.

[. Pierro, Randomised algorithms and probabilistic constraint programming, Proc. of the ERCIM/Compulog Workshop on Constraints, 2000.

[. Pierro and H. Wiklicky, A Banach space based semantics for probabilistic concurrent constraint programming, Proceedings of CATS'98, Computing: the 4th Australian Theory Symposium, 1998.

]. A. Ros95 and . Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, Proceedings of the 8th IEEE Computer Security Foundations Workshop, pp.98-107, 1995.

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.

K. Michael, A. D. Reiter, and . Rubin, Anonymous web transactions with crowds, Commun. ACM, vol.42, issue.2, pp.32-38, 1999.

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

D. Sangiorgi, On the proof method for bisimulation, MFCS, pp.479-488
DOI : 10.1007/3-540-60246-1_153

A. Vijay and . Saraswat, Concurrent Constraint Programming Languages, 1989.

]. S. Sch96 and . Schneider, Security properties and CSP, Proceedings of the IEEE Symposium Security and Privacy, 1996.

[. Selinger, First-order axioms for asynchrony, CONCUR97: Concurrency Theory, pp.376-390, 1997.
DOI : 10.1007/3-540-63141-0_26

D. [. Syverson, M. G. Goldschlag, and . 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.331.3883

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

. A. Vijay, M. Saraswat, P. Rinard, and . Panangaden, Semantic foundations of concurrent constraint programming, Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pp.333-352, 1991.

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

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

D. Sangiorgi and D. Walker, The ?-calculus: a Theory of Mobile Processes, 2001.

]. R. Tix95 and . Tix, Stetige bewertungen auf topologischen räumen. Master's thesis, 1995.