The expressivity of universal timed CCP: undecidability of Monadic FLTL and closure operators for security

ABSTRACT

The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols.

This paper is devoted to the study of 1) the expressiveness of utcc and 2) its semantic foundations. As applications of this study, we also state 3) a noteworthy decidability result for the wellestablished framework of FLTL and 4) bring new semantic insights into the modeling of security protocols.

More precisely, we show that in contrast to tcc, utcc is Turingpowerful by encoding Minsky machines. The encoding uses a monadic constraint system allowing us to prove a new result for a fragment of FLTL: The undecidability of the validity problem for monadic FLTL without equality and function symbols. This result refutes a decidability conjecture for FLTL from a previous paper. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables.

We shall also show that as in tcc, utcc processes can be semantically represented as partial closure operators. The representation is fully abstract wrt the input-output behavior of processes for a meaningful fragment of the utcc. This shows that mobility can be captured as closure operators over an underlying constraint system. As an application we identify a language for security protocols that can be represented as closure operators over a cryptographic constraint system.

REFERENCES

• 1: Martín Abadi, The power of temporal proofs (corrigendum), Theoretical Computer Science, v.70 n.2, p.275-275, Jan 26, 1990 [doi>10.1016/0304-3975(90)90128-5]
• 2: Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM (JACM), v.52 n.1, p.102-146, January 2005 [doi>10.1145/1044731.1044735]
• 3: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols: the spi calculus, Proceedings of the 4th ACM conference on Computer and communications security, p.36-47, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266432]
• 4: Roberto M. Amadio , Denis Lugiez , Vincent Vanackère, On the symbolic reduction of processes with cryptographic functions, Theoretical Computer Science, v.290 n.1, p.695-740, 1 January 2003 [doi>10.1016/S0304-3975(02)00090-7]
• 5: Bruno Blanchet, Security protocols: from linear to classical logic by abstract interpretation, Information Processing Letters, v.95 n.5, p.473-479, 15 September 2005 [doi>10.1016/j.ipl.2005.05.011]
• 6: Michele Boreale , Maria Grazia Buscemi, A method for symbolic analysis of security protocols, Theoretical Computer Science, v.338 n.1-3, p.393-425, 10 June 2005 [doi>10.1016/j.tcs.2005.03.044]
• 7: E. Borger, E. Gradel, and Y. Gurevich. The Classical Decision Problem. Springer, 2001.
• 8: J. R. Buchi. On a decision method in restricted second order arithmetic. In Proc. of Int. Conf. on Logic, Methodology, and Philosophy of Science, 1962.
• 9: Agostino Cortesi , Gilberto Filé , Francesco Ranzato , Roberto Giacobazzi , Catuscia Palamidessi, Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.7-47, Jan. 1997 [doi>10.1145/239912.239914]
• 10: Federico Crazzolara , Glynn Winskel, Petri nets in cryptographic protocols, Proceedings of the 15th International Parallel & Distributed Processing Symposium, p.149, April 23-27, 2001
• 11: Frank S. De Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.685-725, Sept. 1997 [doi>10.1145/265943.265954]
• 12: A. Degtyarev, M. Fisher, and A. Lisitsa. Equality and monodic firstorder temporal logic. Studia Logica, 72(2), 2002.
• 13: Dorothy E. Denning , Giovanni Maria Sacco, Timestamps in key distribution protocols, Communications of the ACM, v.24 n.8, p.533-536, Aug. 1981 [doi>10.1145/358722.358740]
• 14: Marcelo Fiore , Martín Abadi, Computing Symbolic Models for Verifying Cryptographic Protocols, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.160, June 11-13, 2001
• 15: C. Fournet and M. Abadi. Hiding names: Private authentication in the applied pi calculus. In Proc. of ISSS, 2003.
• 16: I. M. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic, 106(1-3), 2000.
• 17: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 18: S. Merz. Decidability and incompleteness results for first-order temporal logics of linear time. Journal of Applied Non-Classical Logics, 2(2), 1992.
• 19: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 20: Marvin L. Minsky, Computation: finite and infinite machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 21: Mogens Nielsen , Catuscia Palamidessi , Frank 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, p.156-167, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571173]
• 22: Mogens Nielsen , Catuscia Palamidessi , Frank D. Valencia, Temporal concurrent constraint programming: denotation, logic and applications, Nordic Journal of Computing, v.9 n.2, p.145-188, Summer 2002
• 23: Carlos Olarte , Frank D. Valencia, Universal concurrent constraint programing: symbolic semantics and applications to security, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil [doi>10.1145/1363686.1363726]
• 24: V. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constraint programming. In Proc. of LICS'94. IEEE CS, 1994.
• 25: Vijay A. Saraswat, Concurrent constraint programming, MIT Press, Cambridge, MA, 1993
• 26: Vijay A. Saraswat , Martin Rinard , Prakash Panangaden, The semantic foundations of concurrent constraint programming, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-352, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99627]
• 27: Andrzej Szalas , Leszek Holenderski, Incompleteness of first-order temporal logic with until, Theoretical Computer Science, v.57 n.2-3, p.317-325, May 1988 [doi>10.1016/0304-3975(88)90045-X]
• 28: Frank D. Valencia, Decidability of infinite-state timed CCP processes and first-order LTL, Theoretical Computer Science, v.330 n.3, p.577-607, 9 February 2005 [doi>10.1016/j.tcs.2004.10.009]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Security, Theory, Verification

Keywords:
closure operators, concurrent constraint programming, first-order linear temporal logic, security protocols