R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I, Information and Computation, vol.100, issue.1, pp.1-40, 1992.
DOI : 10.1016/0890-5401(92)90008-4

M. Reiter and A. Rubin, Crowds: anonymity for Web transactions, ACM Transactions on Information and System Security, vol.1, issue.1, pp.66-92, 1998.
DOI : 10.1145/290163.290168

S. Even, O. Goldreich, and A. Lempel, A randomized protocol for signing contracts, Communications of the ACM, vol.28, issue.6, pp.637-647, 1985.
DOI : 10.1145/3812.3818

O. Herescu and C. Palamidessi, Probabilistic Asynchronous ??-Calculus, Proc. 3rd Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS'00), ser, pp.146-160, 2000.
DOI : 10.1007/3-540-46432-8_10

URL : http://arxiv.org/pdf/cs/0109002v1.pdf

K. Chatzikokolakis and C. Palamidessi, A framework to analyze probabilistic protocols and its application to the partial secrets exchange, Proc. Int. Symp. Trustworthy Global Computing (TGC'05), ser. Lecture Notes in Computer Science, pp.146-162, 2005.

M. Bhargava and C. Palamidessi, Probabilistic anonymity Concurrency Theory (CONCUR'05), ser. Lecture Notes in Computer Science, Proc. 16th Int. Conf, pp.171-185, 2005.

C. Priami, Stochastic ??-Calculus, The Computer Journal, vol.38, issue.7, pp.578-589, 1995.
DOI : 10.1093/comjnl/38.7.578

A. Regev, W. Silverman, and E. Shapiro, Representation and simulation of biochemical processes using the ??-calculus process algebra, Biocomputing 2001, pp.459-470, 2001.
DOI : 10.1142/9789814447362_0045

C. Priami, A. Regev, W. Silverman, and E. Shapiro, Application of a stochastic name-passing calculus to representation and simulation of molecular processes, Information Processing Letters, vol.80, issue.1, pp.25-31, 2001.
DOI : 10.1016/S0020-0190(01)00214-9

P. Yang, C. Ramakrishnam, and S. Smolka, A logic encoding of the ?-calculus: model checking mobile processes using tabled resolution, Int. Journal on Software Tools Technology Transfer, vol.4, pp.1-29, 2004.

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), ser. Lecture Notes in Computer Science, H. Hermanns and J. Palsberg, pp.441-444, 2006.
DOI : 10.1007/11691372_29

B. Victor and F. Moller, The Mobility Workbench -a tool for the ?calculus, Proc. 6th Int. Conf. Computer Aided Verification (CAV'94), ser. Lecture Notes in Computer Science, pp.428-440, 1994.

B. Blanchet, ProVerif: Automatic cryptographic protocol verifier user manual, 2005.

S. Chaki, S. Rajamani, and J. Rehof, Types as models: Model checking message-passing programs, Proc. 29th Symp. Principles of Programming Languages (POPL'02, pp.45-57, 2002.

P. Wu, Interpreting ?-calculus with Spin/Promela, Computer Science, vol.8, pp.7-9, 2003.

H. Song and K. Compton, Verifying ?-calculus processes by Promela translation, 2003.

A. Venet, Abstract interpretation of the pi-calculus, Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, ser. LNCS, M. Dam, pp.51-75, 1996.

C. Bodei, P. Degano, F. Nielson, and H. R. Nielson, Static analysis for the pi-calculus with applications to security, Information and Computation, vol.165, pp.68-92, 2001.

]. A. Phillips and L. Cardelli, Efficient, Correct Simulation of Biological Processes in the Stochastic Pi-calculus, Proc. 5th Int. Workshop Computational Methods in Systems Biology (CMSB'07), ser. Lecture Notes in, pp.184-199, 2007.
DOI : 10.1007/978-3-540-75140-3_13

G. Norman, C. Palamidessi, D. Parker, and P. Wu, Model checking the probabilistic pi-calculus, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), pp.169-178, 2007.
DOI : 10.1109/QEST.2007.31

URL : https://hal.archives-ouvertes.fr/inria-00201069

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

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

M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, vol.138, issue.2, pp.353-389, 1995.
DOI : 10.1016/0304-3975(94)00172-F

URL : http://doi.org/10.1016/0304-3975(94)00172-f

P. Wu, C. Palamidessi, and H. Lin, Symbolic Bisimulations for Probabilistic Systems, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), pp.179-188, 2007.
DOI : 10.1109/QEST.2007.11

H. Lin, Symbolic bisimulation and proof systems for the ?-calculus, 1994.

M. Boreale and R. D. Nicola, A Symbolic Semantics for the ??-calculus, Information and Computation, vol.126, issue.1, pp.34-52, 1996.
DOI : 10.1007/978-3-540-48654-1_24

H. Lin, Complete inference systems for weak bisimulation equivalences in the ??-calculus, Information and Computation, vol.180, issue.1, pp.1-29, 2003.
DOI : 10.1016/S0890-5401(02)00014-7

A. Ingólfsdóttir and H. Lin, A Symbolic Approach to Value-Passing Processes, Handbook of Processes Algebra, 2001.
DOI : 10.1016/B978-044482830-9/50025-4

J. Hillston, A Compositional Approach to Performance Modelling, 1996.
DOI : 10.1017/CBO9780511569951

G. Norman, C. Palamidessi, D. Parker, and P. Wu, Translating the probabilistic ?-calculus to PRISM, 2007.

A. Roscoe, The theory and practice of concurrency, 1997.

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994.
DOI : 10.1007/BF01211866

A. Bianco and L. De-alfaro, Model checking of probabilistic and nondeterministic systems, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science, ser, pp.499-513, 1995.
DOI : 10.1007/3-540-60692-0_70

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Verifying continuous time Markov chains, Proc. 8th Int. Conf. Computer Aided Verification (CAV'96), ser, pp.269-276, 1996.
DOI : 10.1007/3-540-61474-5_75

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3391

C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, Model-checking algorithms for continuous-time markov chains, IEEE Transactions on Software Engineering, vol.29, issue.6, pp.524-541, 2003.
DOI : 10.1109/TSE.2003.1205180

M. Goldsmith, N. Moffat, B. Roscoe, T. Whitworth, and I. Zakiuddin, Watchdog Transformations for Property-Oriented Model-Checking, Proc. 2th Int. Symp. Formal Methods Europe (FME'03), ser. Lecture Notes in Computer Science, pp.600-616, 2003.
DOI : 10.1007/978-3-540-45236-2_33

L. Caires and L. Cardelli, A spatial logic for concurrency (part I), Information and Computation, vol.186, issue.2, pp.194-235, 2003.
DOI : 10.1016/S0890-5401(03)00137-8

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

G. Norman and V. Shmatikov, Analysis of Probabilistic Contract Signing, Journal of Computer Security, vol.14, issue.6, pp.561-589, 2006.
DOI : 10.1007/978-3-540-40981-6_9

F. Orava and J. Parrow, An algebraic verification of a mobile network, Formal Aspects of Computing, vol.5, issue.1, pp.497-543, 1992.
DOI : 10.1007/BF01211473

C. Priami, Stochastic analysis of mobile telephony networks, Proc. 5th Int. Workshop on Process Algebra and Performance Modeling (PAPM'97, pp.145-171, 1997.

J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, Probabilistic model checking of complex biological pathways, Proc. 4th Int. Workshop Computational Methods in Systems Biology (CMSB'06), ser. Lecture Notes in Bioinformatics, C. Priami, pp.32-47, 2006.