A. Armando and L. Compagna, SAT-based model-checking for security protocols analysis, International Journal of Information Security, vol.9, issue.1, pp.3-32, 2008.
DOI : 10.1007/s10207-007-0041-y

T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard, Two classes of Boolean functions for dependency analysis, Science of Computer Programming, vol.31, issue.1, pp.3-45, 1998.
DOI : 10.1016/S0167-6423(96)00039-1

G. Berry and G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, vol.19, issue.2, pp.87-152, 1992.
DOI : 10.1016/0167-6423(92)90005-V
URL : https://hal.archives-ouvertes.fr/inria-00075711

C. Bodei, L. Brodo, P. Degano, and H. Gao, Detecting and preventing type flaws at static time*, Journal of Computer Security, vol.18, issue.2, pp.229-264, 2010.
DOI : 10.3233/JCS-2010-0361
URL : http://doi.org/10.3233/jcs-2010-0361

M. Boreale, Symbolic Trace Analysis of Cryptographic Protocols, LNCS, vol.2076, pp.667-681, 2001.
DOI : 10.1007/3-540-48224-5_55

M. Codish and B. Demoen, Deriving polymorphic type dependencies for logic programs using multiple incarnations of Prop, LNCS, vol.864, pp.281-296, 1994.
DOI : 10.1007/3-540-58485-4_47

M. M. Codish and K. Marriott, Suspension analyses for concurrent logic programs, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.649-686, 1994.
DOI : 10.1145/177492.177656

M. M. Codish, K. Marriott, and W. Winsborough, A confluent semantic basis for the analysis of concurrent constraint logic programs, The Journal of Logic Programming, vol.30, issue.1, pp.53-81, 1997.
DOI : 10.1016/S0743-1066(96)00013-1

M. Codish, H. Søndergaard, and P. Stuckey, Sharing and groundness dependencies in logic programs, ACM Transactions on Programming Languages and Systems, vol.21, issue.5, pp.948-976, 1999.
DOI : 10.1145/330249.330252

M. Comini, L. Titolo, and A. Villanueva, Abstract, Theory and Practice of Logic Programming, vol.11, issue.4-5, pp.4-5, 2011.
DOI : 10.1017/S1471068411000135

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

P. Cousot and R. Cousot, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.103-179, 1992.
DOI : 10.1016/0743-1066(92)90030-7
URL : http://doi.org/10.1016/0743-1066(92)90030-7

F. S. De-boer, M. Gabbrielli, E. Marchiori, and C. Palamidessi, Proving concurrent constraint programs correct, ACM Transactions on Programming Languages and Systems, vol.19, issue.5, pp.685-725, 1997.
DOI : 10.1145/265943.265954

F. S. De-boer, M. Gabbrielli, and M. C. Meo, A Timed Concurrent Constraint Language, Information and Computation, vol.161, issue.1, pp.45-83, 2000.
DOI : 10.1006/inco.1999.2879

F. S. De-boer, A. D. Pierro, and C. Palamidessi, Nondeterminism and infinite computations in constraint programming, Theoretical Computer Science, vol.151, issue.1, pp.37-78, 1995.
DOI : 10.1016/0304-3975(95)00047-Z

D. Dolev and A. C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1983.
DOI : 10.1109/TIT.1983.1056650

S. Escobar, C. Meadows, and J. Meseguer, State space reduction in the maude-nrl protocol analyzer, 2011.

F. Fag-e-s, P. Ruet, and S. Soliman, Linear Concurrent Constraint Programming: Operational and Phase Semantics, Information and Computation, vol.165, issue.1, pp.14-41, 2001.
DOI : 10.1006/inco.2000.3002

M. Gabbrielli, M. Marriott, K. Palamidessi, and C. , Compositional analysis for concurrent constraint programming, LICS.I E E EC o m p u t e r Society, pp.210-221, 1993.

M. Gabbrielli, M. Marriott, K. Palamidessi, and C. , Confluence in concurrent constraint programming, Theoretical Computer Science, vol.183, issue.2, pp.281-315, 1997.

M. Gabbrielli, M. Marriott, K. Palamidessi, and C. , Constraint logic programming with dynamic scheduling: A semantics based on closure operators, Inf. Comput, vol.137, issue.1, pp.41-67, 1997.

M. Olarte, C. Palamidessi, and C. , A framework for abstract interpretation of timed concurrent constraint programs, pp.207-218, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00426608

M. Olarte, C. Palamidessi, C. Valencia, and F. , Declarative diagnosis of temporal concurrent constraint programs, LNCS, vol.4670, pp.271-285, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00201065

A. Va, Automatic verification of timed concurrent constraint programs, pp.265-300, 2006.

M. P. Fiore and M. Abadi, Computing symbolic models for verifying cryptographic protocols, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.0-1, 2001.
DOI : 10.1109/CSFW.2001.930144
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.3750

R. Giacobazzi, S. K. Debray, L. , and G. , Generalized semantics and abstract interpretation for constraint logic programs, The Journal of Logic Programming, vol.25, issue.3, pp.191-247, 1995.
DOI : 10.1016/0743-1066(95)00038-0
URL : http://doi.org/10.1016/0743-1066(95)00038-0

R. Haemmerlé, F. Fag-e-s, and S. Soliman, Closures and Modules Within Linear Logic Concurrent Constraint Programming, LNCS, vol.4855, pp.544-556, 2007.
DOI : 10.1007/978-3-540-77050-3_45

P. V. Hentenryck, V. A. Saraswat, and Y. Deville, Design, implementation, and evaluation of the constraint language cc(FD), Journal of Logic Programming, vol.37, pp.1-3, 1998.
DOI : 10.1007/3-540-59155-9_15

T. Hildebrandt and H. A. López, Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming, LNCS, vol.100, issue.3, pp.417-431, 2009.
DOI : 10.1016/0890-5401(92)90008-4

J. Jaffar and J. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, pp.111-119, 1987.
DOI : 10.1145/41625.41635

R. Jagadeesan, W. Marrero, C. Pitcher, and V. A. Saraswat, Timed constraint programming, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.164-175, 2005.
DOI : 10.1145/1069774.1069790

H. A. López, C. Olarte, and J. A. Pérez, Towards a Unified Framework for Declarative Structured Communications, Electronic Proceedings in Theoretical Computer Science, vol.17, pp.1-15, 2009.
DOI : 10.4204/EPTCS.17.1

G. Lowe, Breaking and fixing the needham-schroeder public-key protocol using fdr. Software -Concepts and Tools 17, pp.93-102, 1996.

M. J. Maher, Complete axiomatizations of the algebras of finite, rational and infinite trees, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.8-11, 1988.
DOI : 10.1109/LICS.1988.5132

N. P. Mendler, P. Panangaden, P. J. Scott, and R. A. Seely, A logical view of concurrent constraint programming, Nordic Journal of Computing, vol.2, issue.2, pp.181-220, 1995.

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. Nielsen, C. Palamidessi, and F. Valencia, Temporal concurrent constraint programming: Denotation, logic and applications, Nordic J. of Computing, vol.9, issue.1, pp.145-188, 2002.
DOI : 10.7146/brics.v8i48.21708
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.3124

M. Nielsen, C. Palamidessi, and F. D. Valencia, On the expressive power of temporal concurrent constraint programming languages, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '02, pp.5-6, 2002.
DOI : 10.1145/571157.571173

C. Olarte, C. Rueda, and F. D. Valencia, Models and emerging trends of concurrent constraint programming, Constraints, vol.340, issue.3, pp.535-578, 2013.
DOI : 10.1007/s10601-013-9145-3
URL : https://hal.archives-ouvertes.fr/hal-00869192

C. Olarte and F. D. Valencia, The expressivity of universal timed CCP, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.8-19, 2008.
DOI : 10.1145/1389449.1389452
URL : https://hal.archives-ouvertes.fr/inria-00349353

C. Olarte and F. D. Valencia, Universal concurrent constraint programing, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.145-150, 2008.
DOI : 10.1145/1363686.1363726
URL : https://hal.archives-ouvertes.fr/inria-00201497

V. A. Saraswat, Concurrent constraint programming, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1993.
DOI : 10.1145/96709.96733

V. A. Saraswat, R. Jagadeesan, and V. Gupta, Foundations of timed concurrent constraint programming, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.1-8, 1994.
DOI : 10.1109/LICS.1994.316085

V. A. Saraswat, M. C. Rinard, and P. Panangaden, The semantic foundations of concurrent constraint programming, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.333-352, 1991.
DOI : 10.1145/99583.99627

T. Sato and H. Tamaki, Enumeration of Success Patterns in Logic Programs, Theoretical Computer Science, vol.342, pp.2-7, 1984.

E. Y. Shapiro, The family of concurrent logic programming languages, ACM Computing Surveys, vol.21, issue.3, pp.413-510, 1989.
DOI : 10.1145/72551.72555

G. Smolka, A foundation for higher-order concurrent constraint programming, LNCS, vol.845, pp.50-72, 1994.

D. X. Song, S. Berezin, and A. Perrig, Athena: a novel approach to efficient automatic security protocol analysis1, Journal of Computer Security, vol.9, issue.1-2, pp.47-74, 2001.
DOI : 10.3233/JCS-2001-91-203

S. Tini, On the expressiveness of Timed Concurrent Constraint Programming, Electronic Notes in Theoretical Computer Science, vol.27, pp.3-4, 1999.
DOI : 10.1016/S1571-0661(05)80291-9

E. Zaffanella, R. Giacobazzi, L. , and G. , Abstracting synchronization in concurrent constraint programming, Journal of Functional and Logic Programming, vol.6, 1997.
DOI : 10.1007/3-540-58402-1_6

P. Case, Consider the following derivation h~ y ;(local ~ x ) Q; di? !h~ y [ ~ x ; Q; di? ! ? h~ y [ ~ x 0 ; Q 0 ; d 0 i6 ? ! where, by alpha-conversion, ~ x \ ~ y = ; and ~ x \ fv (d)=;. Assume that 9~ y (d) ? = 9~ y 9~ x 0 (d 0 ) Since the derivation starting from Q is shorter than that starting from P , we conclude 9~ y (d)

P. Case and Q. Next, This case is trivial since d

P. Case and Q. Unless-c-next, We distinguish two cases: (1) If d ` c,t h e nw eh a v e h~ x ; unless c next Q; di? !h ~ x ; skip

D. Let, P be a locally independent program s.t. d.s 2 [[ P ]] . I f P (d,d 0 ) ==== ) R then d 0 ? = d and s

P. Case and Q. Next, This case is trivial since h~ x ; P ; di 6 ?! for any d and ~ x and F (P )=Q

P. Case and Q. Unless-c-next, If d ` c the case is trivial

P. Case, Assume that p(~ x ):?Q 2D.I fd By using the rule R CALL we can show that there is a derivation h~ y ; p(~ x ); di? !h~ y ; Q

P. Case and . Skip, This case is trivial

P. Case and R. , We must have that s 2 By inductive hypothesis we know that s ? 2

P. Case, It must be the case that there exists d 0 .s 0 ~ x -variant of d.s s.t. d 0 Then, by (structural) inductive hypothesis ?(d 0 .s 0 ) 2

P. Case, Ifd 0 ` c(~ y ) then, by monotonicity, 9~ x (d 0 ) `9~ x (c(~ y )) and then 9~ x (d) ` c(~ y ) Hence, it must be the case that d ` c(~ y ) and d.s 2, then 9~ x (d 0 ) 6 ` c(~ y )( s i n c e 9~ x (d 0 ) ? d 0 ). Hence, d 6 ` c(~ y ) and trivially, p.2