M. Abadi, B. Blanchet, and C. Fournet, Just Fast Keying in the Pi-Calculus, ACM Trans. Inf. Syst. Secur, vol.10, issue.3, 2007.

R. Banach, J. Balazs, and G. Papadoupolous, A Translation of the Pi-Calculus Into MONSTR, J. UCS, vol.1, issue.6, pp.339-398, 1995.
DOI : 10.1007/978-3-642-80350-5_32

D. Bergamini, N. Descoubes, C. Joubert, and R. Mateescu, BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking, Proc. of TACAS'05, pp.581-585, 2005.
DOI : 10.1007/978-3-540-31980-1_42
URL : https://hal.archives-ouvertes.fr/hal-00685325

D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, F. Lang et al., Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.0) INRIA/VASY, 2010.

M. Dam, On the decidability of process equivalences for the ??-calculus, Theoretical Computer Science, vol.183, issue.2, pp.215-228, 1997.
DOI : 10.1016/S0304-3975(96)00325-8

S. Deng, Z. Wu, M. Zhou, Y. Li, and J. Wu, Modeling Service Compatibility with Pi-calculus for Choreography, Proc. of ER'06, pp.26-39, 2006.
DOI : 10.1007/11901181_4

G. L. Ferrari, G. Ferro, S. Gnesi, U. Montanari, M. Pistore et al., An Automated Based Verification Environment for Mobile Processes, Proc. of TACAS'97, pp.275-289, 1997.

L. Fredlund and F. Orava, Modelling Dynamic Communication Structures in LOTOS, Proc. of FORTE'91, volume C-2 of IFIP Transactions, pp.185-200, 1991.
DOI : 10.1016/B978-0-444-89402-1.50023-0

H. Garavel, . Open, and . Caesar, An Open Software Architecture for Verification, Simulation, and Testing, Proc. of TACAS'98, pp.68-84, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073337

H. Garavel, F. Lang, and R. Mateescu, Compiler Construction Using LOTOS NT, Proc. of CC'02, pp.9-13, 2002.
DOI : 10.1007/3-540-45937-5_3

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, Proc. of CAV'07, pp.158-163, 2007.
DOI : 10.1007/978-3-540-73368-3_18
URL : https://hal.archives-ouvertes.fr/inria-00189021

H. Garavel and M. Sighireanu, A Graphical Parallel Composition Operator for Process Algebras, Proc. of FORTE/PSTV'99, pp.185-202, 1999.
DOI : 10.1007/978-0-387-35578-8_11

R. Lucchi and M. Mazzara, A pi-calculus based semantics for WS-BPEL, The Journal of Logic and Algebraic Programming, vol.70, issue.1, pp.96-118, 2007.
DOI : 10.1016/j.jlap.2006.05.007

I. Iec, Enhancements to LOTOS (E-LOTOS) International Standard 15437, International Organization for Standardization, 2001.

I. Iec, LOTOS ? A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, International Standard International Organization for Standardization, vol.8807, 1989.

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, Proc. of FM'08, pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12
URL : https://hal.archives-ouvertes.fr/inria-00315312

R. Milner, Communication and Concurrency, 1989.

R. Milner, Communicating and Mobile Systems: the Pi-Calculus, 1999.

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

U. Montanari and M. Pistore, Checking Bisimilarity for Finitary Pi-Calculus, Proc. of CONCUR'95, pp.42-56, 1995.
DOI : 10.1007/3-540-60218-6_4

E. Najm, J. Stefani, and A. Février, Towards a mobile LOTOS, Proc. of FORTE'95 IFIP Conference Proceedings, pp.127-142, 1995.
DOI : 10.1007/978-0-387-34945-9_10

G. Norman, C. Palamidessi, D. Parker, and P. Wu, Model Checking Probabilistic and Stochastic Extensions of the π-Calculus, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.209-223, 2009.
DOI : 10.1109/TSE.2008.77

J. Parrow, An introduction to the pi-calculus, Handbook of Process Algebra, pp.479-544, 2001.

F. Puhlmann, Why Do We Actually Need the Pi-Calculus for Business Process Management?, Proc. of BIS'06, pp.77-89, 2006.

D. Sangiorgi, A theory of bisimulation for the ??-calculus, Acta Informatica, vol.XVI, issue.2, pp.69-97, 1996.
DOI : 10.1007/s002360050036

H. Song and K. J. Compton, Verifying Pi-Calculus Processes by Promela Translation, 2003.

B. Victor and F. Moller, The mobility workbench ??? A tool for the ??-Calculus, Proc. of CAV'94, pp.428-440, 1994.
DOI : 10.1007/3-540-58179-0_73

P. Wu, Interpreting Pi-Calculus with Spin/Promela, Proc. of NCTCS'03, pp.7-9, 2003.

P. Yang, C. R. Ramakrishnan, and S. A. Smolka, A logical encoding of the ??-calculus: model checking mobile processes using tabled resolution, International Journal on Software Tools for Technology Transfer, vol.7, issue.1, pp.38-66, 2004.
DOI : 10.1007/s10009-003-0136-3

A. Dispatcher, W. S. Translated, and L. Nt, We show below an excerpt of the Lotos NT code (processes MAIN and Dispatcher 4 corresponding to the agents Main and Dispatcher ) generated by the Pic2Lnt translator from the ?-calculus specification of the dispatcher Web service given in Section 5. The names of Lotos NT processes are indexed by the number of gates in G (not counting the G pub and G priv gates). process MAIN [PUBLIC,PRIVATE:any] is var req, a, b, c:Chan in req:=req(new_id()); a:=a(new_id()), p.=b(new_id=c(new_id(

|. Dispatcher_4, [. Public, G. Private, G. , G. Server_3 et al., 14) end par end hide || Server_231) end par end hide end var end process process Dispatcher_4G3:any](req:Chan,pid:Nat) is select var k,x:Chan, s:Nat in G0 (!req, ?k, ?x, ?s, !pid) [] G1 (!req, ?k, ?x, ?s, !pid) [] G2 (!req, ?k, ?x, ?s, !pid) [] G3 (!req, ?k, ?x, ?s, !pid) [] PUBLIC (!req, ?k, ?x, !false) where is_public(req) [] PRIVATE (!req, ?k, ?x, !false) where not(is_public(req)) end select ; select var r, G3 (!k, !x, !pid, ?r) [] PUBLIC (!k, !x, !true) where is_public(k) [] PRIVATE (!k, !x, !true) where not(is_public(k)) end select, p.3