. Moreover, J, there exists b ? B s , such that i( j 1 , b) = i( j 2 , b), otherwise we would have v j 1 = v j 2 . Let u be an abstract computation unit. We want to compute the set F of the pairs ((v j ) j?J , i ? J × B ? 0; n) such that there exists a computation unit u and a family of distinct computation units

?. Thus, Ct k ) ? ? N V c (? N V c (continuation k ))). By Prop. 9.2.2 and marker unambiguity, we get that: ? N V c (?, new_threads)

. Prop, 9.2.2 and marker unambiguity, we get that: ? N V c (u.? ,C \ rem_threads ? new_threads) ? ? N V c (v )

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. POPL'01, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

M. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, 1997.
DOI : 10.1145/266420.266432

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

Y. Y. Benjamin and . Aziz, A static analysis of cryptographic processes : the denotational approach Journal of Logic and Algebraic Programming, special issue on Modelling and Verification of Cryptographic Protocols

Y. Y. Benjamin and . Aziz, A Static Analysis Framework for Security Properties in Mobile and Cryptographic Systems, 2003.

Y. Y. Benjamin, G. W. Aziz, and . Hamilton, A privacy analysis for the pi-calculus : The denotational approach, Proc. SAVE'02, number 94 in Datalogiske Skrifter, 2002.

B. Blanchet, From Secrecy to Authenticity in Security Protocols, Proc. SAS'02, 2002.
DOI : 10.1007/3-540-45789-5_25

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proc. PLDI'03, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

C. Bodei, P. Degano, F. Nielson, and H. Nielson, Control flow analysis for the ??-calculus, Proc. CONCUR'98, 1998.
DOI : 10.1007/BFb0055617

C. Bodei, P. Degano, F. Nielson, and H. Nielson, Static Analysis of Processes for No Read-Up and No Write-Down, Proc. FoSSaCS'99, 1999.
DOI : 10.1007/3-540-49019-1_9

C. Bodei, P. Degano, F. Nielson, and H. Nielson, Static Analysis for the ??-Calculus with Applications to Security, Information and Computation, vol.168, issue.1, 2000.
DOI : 10.1006/inco.2000.3020

M. Bugliesi, G. Castagna, and S. Crafa, Boxed Ambients, Proc. TACS'01, number 2215 in LNCS, pp.38-63, 2001.
DOI : 10.1007/3-540-45500-0_2
URL : https://hal.archives-ouvertes.fr/hal-00152525

M. Bugliesi, G. Castagna, and S. Crafa, Access control for mobile agents, ACM Transactions on Programming Languages and Systems, vol.26, issue.1, 2004.
DOI : 10.1145/963778.963781
URL : https://hal.archives-ouvertes.fr/hal-00152525

L. Cardelli, G. Ghelli, and A. D. Gordon, Ambient Groups and Mobility Types, Proc. TCS'00, 2000.
DOI : 10.1007/3-540-44929-9_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.8002

L. Cardelli, G. Ghelli, and A. D. Gordon, Secrecy and group creation, Proc. CONCUR'00, 2000.
DOI : 10.1016/s1571-0661(05)80034-9
URL : http://doi.org/10.1016/s1571-0661(05)80034-9

L. Cardelli and A. D. Gordon, Mobile ambients, Theoretical Computer Science, vol.240, issue.1, 1998.
DOI : 10.1016/s1571-0661(05)80699-1
URL : http://doi.org/10.1016/s1571-0661(05)80699-1

S. Chaki, S. K. Rajamani, and J. Rehof, Types as models : Model checking message-passing programs, Proc. POPL'02, 2002.

W. Charatonik, A. D. Gordon, and J. M. Talbot, Finite-Control Mobile Ambients, Proc. ESOP'02, number 2305 in LNCS, 2002.
DOI : 10.1007/3-540-45927-8_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.2483

C. Chiu, J. Ho-man, and . Lee, Interval linear constraint solving using the preconditioned interval Gauss-Seidel method, Proc. ICLP'95, Logic Programming, 1995.

P. Cousot, Semantic foundations of program analysis In Program Flow Analysis : Theory and Applications, chapter 10, 1981.

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proceedings of the Second International Symposium on Programming, pp.106-130, 1976.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

P. Cousot and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, 1992.
DOI : 10.1093/logcom/2.4.511

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Proc. PLILP'92, 1992.
DOI : 10.1007/3-540-55844-6_142

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, 1978.
DOI : 10.1145/512760.512770

M. Dam, Model Checking Mobile Processes, Information and Computation, vol.129, issue.1, pp.35-51, 1996.
DOI : 10.1006/inco.1996.0072
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.4808

V. Danos and S. Pradalier, Projective Brane Calculus, Proc. CMSB'04
DOI : 10.1021/j100540a008
URL : https://hal.archives-ouvertes.fr/hal-00164593

N. Govert-de-bruijn, Lambda-calculus notation with nameless dummies : a tool for automatic formula manipulation with application to the Church-Rosser theorem, Indagationes Mathematicae, vol.34, issue.5, 1972.

N. Dershowitz and J. Jouannaud, Rewrite systems In Handbook of Theoretical Computer Science, Volume B : Formal Models and Sematics (B), 1990.

D. Dolev and A. Yao, On the security of public key protocols (extended abstract), Proc. FOCS'81, 1981.

J. Feret, Abstract interpretation of mobile systems Journal of Logic and Algebraic Programming, special issue on pi-calculus

J. Feret, amb-s.a : a static analyzer for mobile ambients, Prototype

J. Feret, Conception de ?-sa : un analyseur statique générique pour le ?-calcul. Graduate thesis, École Polytechnique, september 1999

J. Feret, Confidentiality Analysis of Mobile Systems, Proc. SAS'00, number 1824 in LNCS, 2000.
DOI : 10.1007/978-3-540-45099-3_8
URL : https://hal.archives-ouvertes.fr/inria-00527941

J. Feret, Abstract Interpretation-Based Static Analysis of Mobile Ambients, Eighth International Static Analysis Symposium (SAS'01), number 2126 in LNCS, 2001.
DOI : 10.1007/3-540-47764-0_24
URL : https://hal.archives-ouvertes.fr/inria-00527929

J. Feret, Occurrence Counting Analysis for the ??-calculus, Proc. GETCO'00, 2001.
DOI : 10.1016/S1571-0661(05)01155-2
URL : https://hal.archives-ouvertes.fr/inria-00527933

J. Feret, Dependency Analysis of Mobile Systems, Proc. ESOP'02, number 2305 in LNCS, 2002.
DOI : 10.1007/3-540-45927-8_22
URL : https://hal.archives-ouvertes.fr/inria-00527924

C. Fournet, The Join-Calculus : A Calculus for Distributed Mobile Programming, 1998.

C. Fournet and G. Gonthier, The reflexive CHAM and the joincalculus, Proc. POPL'96, 1996.

P. Granger, Static analysis of linear congruence equalities among variables of a program, Proc. TAPSOFT'91, 1991.
DOI : 10.1007/3-540-53982-4_10

J. René-rydhof-hansen, F. Grydholt-jensen, H. Nielson, and . Nielson, Abstract Interpretation of Mobile Ambients, Proc. SAS'99, 1999.
DOI : 10.1007/3-540-48294-6_9

M. Hennessy and J. Riely, Resource access control in systems of mobile agents, Proc. HLCL'98, 1998.

M. Hennessy and J. Riely, A typed language for distributed mobile processes, Proc. POPL'98, 1998.

A. Igarashi and N. Kobayashi, A generic type system for the ?calculus, Proc. POPL'01, 2001.

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, 1976.
DOI : 10.1007/BF00268497

C. Laneve and B. Victor, Solos in concert, Proc. ICALP'99, 1999.
DOI : 10.1007/3-540-48523-6_48

C. Laneve and B. Victor, Solos in concert, Mathematical Structures in Computer Science, vol.13, issue.5, 2003.
DOI : 10.1007/3-540-48523-6_48

F. Levi and S. Maffeis, An Abstract Interpretation Framework for Analysing Mobile Ambients, Proc. SAS'01, 2001.
DOI : 10.1007/3-540-47764-0_23

F. Levi and S. Maffeis, On abstract interpretation of Mobile Ambients, Information and Computation, vol.188, issue.2, 2004.
DOI : 10.1016/j.ic.2003.06.001

F. Levi and D. Sangiorgi, Controlling interference in ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, 2000.
DOI : 10.1145/325694.325741

L. Mauborgne and . Astrée, Verification of absence of run-time error The International Federation for Information Processing, Building the information Society (18th IFIP World Computer Congress), pp.384-392, 2004.

R. Milner, The Polyadic ??-Calculus: a Tutorial, Proceedings of the International Summer School on Logic and Algebra of Specification, 1991.
DOI : 10.1007/978-3-642-58041-3_6

A. Miné, The octagon abstract domain, Proc. AST'01 in WCRE'01, 2001.

A. Miné, A Few Graph-Based Relational Numerical Abstract Domains, Proc. SAS'02, 2002.
DOI : 10.1007/3-540-45789-5_11

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, Proc. ESOP'04, 2004.
DOI : 10.1007/978-3-540-24725-8_2

A. Miné, Weakly Relational Numerical Abstract Domains, 2004.

F. Nielson, H. R. Nielson, R. R. Hansen, and J. Jensen, Validating Firewalls in Mobile Ambients, Proc. CONCUR'99, 1999.
DOI : 10.1007/3-540-48320-9_32

F. Nielson, H. R. Nielson, and H. Pilegaard, Spatial Analysis of BioAmbients, Proc. SAS'04, 2004.
DOI : 10.1007/978-3-540-27864-1_8

F. Nielson, H. R. Nielson, and H. Seidl, Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi, Proc. SAS'02, 2002.
DOI : 10.1007/3-540-45789-5_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.1256

F. Nielson and H. Seidl, Control-Flow Analysis in Cubic Time, Proc. ESOP'01, 2001.
DOI : 10.1007/3-540-45309-1_17

H. Nielson and F. Nielson, Shape analysis for mobile ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, 2000.
DOI : 10.1145/325694.325711

J. Rohit and . Parikh, On context-free languages, Journal of the ACM, vol.13, 1966.

J. Parrow and B. Victor, The fusion calculus: expressiveness and symmetry in mobile processes, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), 1998.
DOI : 10.1109/LICS.1998.705654

A. T. Phillips, N. Yoshida, and S. Eisenbach, A Distributed Abstract Machine for Boxed Ambient Calculi, Proc. ESOP'04, 2004.
DOI : 10.1007/978-3-540-24725-8_12

K. Sriram, J. Rajamani, and . Rehof, A behavioral module system for the ?-calculus, Proc. SAS'01, 2001.

A. Regev, E. M. Panina, W. Silverman, L. Cardelli, and E. Y. Shapiro, BioAmbients: an abstraction for biological compartments, Theoretical Computer Science, vol.325, issue.1, pp.141-167, 2004.
DOI : 10.1016/j.tcs.2004.03.061
URL : http://doi.org/10.1016/j.tcs.2004.03.061

J. Cortadella and R. Clarisó, The octahedron abstract domain, Proc. SAS'04, 2004.

D. Sangiorgi, From ??-calculus to higher-order ??-calculus ??? and back, Proc. TAPSOFT'93, 1993.
DOI : 10.1007/3-540-56610-4_62
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.946

D. Sangiorgi and A. Valente, A Distributed Abstract Machine for Safe Ambients, Proc. ICALP'01, 2001.
DOI : 10.1007/3-540-48224-5_34

N. David and . Turner, The Polymorphic ?-Calculus : Theory and Implementation, 1995.

A. Venet, Abstract interpretation of the ??-calculus, Proc. LO- MAPS'97, 1997.
DOI : 10.1007/3-540-62503-8_3

A. Venet, Automatic Determination of Communication Topologies in Mobile Systems, Proc. SAS'98, 1998.
DOI : 10.1007/3-540-49727-7_9

J. Vitek and G. Castagna, Seal: A Framework for Secure Mobile Computations, Proc. IPL'99, 1999.
DOI : 10.1007/3-540-47959-7_3

Y. C. Thomas, S. S. Woo, and . Lam, Authentication for distributed systems, Internet besieged : countering cyberspace scofflaws, pp.319-355, 1998.