Universal concurrent constraint programing

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Universal concurrent constraint programing: symbolic semantics and applications to security

Full text

Pdf (317 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2008 ACM symposium on Applied computing table of contents

Fortaleza, Ceara, Brazil

SESSION: Constraint satisfation and programming table of contents

Pages 145-150

Year of Publication: 2008

ISBN:978-1-59593-753-7

Authors

Carlos Olarte	Pontificia Universidad Javeriana
Frank D. Valencia	CNRS and LIX École Polytechnique

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 36, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1363686.1363726 What is a DOI?

ABSTRACT

We introduce the Universal Timed Concurrent Constraint Programming (utcc) process calculus; a generalisation of Timed Concurrent Constraint Programming. The utcc calculus allows for the specification of mobile behaviours in the sense of Milner's π-calculus: Generation and communication of private channels or links. We first endow utcc with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. We also show that utcc has a strong connection with Pnueli's Temporal Logic. This connection can be used to prove reachability properties of utcc processes. As a compelling example, we use utcc to exhibit the secrecy flaw of the Needham-Schroeder security protocol.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	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]
	2	Michele Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.667-681, July 08-12, 2001
	3	Federico Crazzolara , Glynn Winskel, Events in security protocols, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.501998]
	4	François Fages , Paul Ruet , Sylvain Soliman, Linear concurrent constraint programming: operational and phase semantics, Information and Computation, v.165 n.1, p.14-41, Feb. 25, 2001 [doi>10.1006/inco.2000.3002]
	5	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
	6	Cosimo Laneve , Ugo Montanari, Mobility in the CC-Paradigm, Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science, p.336-345, August 24-28, 1992
	7	Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
	8	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	9	Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
	10	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
	11	Catuscia Palamidessi , Vijay Saraswat , Frank D. Valencia , Bjorn Victor, On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.59-68, August 12-15, 2006 [doi>10.1109/LICS.2006.39]
	12	V. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constraint programming. In Proc. of LICS'94. IEEE CS, 1994.
	13	Vijay A. Saraswat, Concurrent constraint programming, MIT Press, Cambridge, MA, 1993
	14	K. Ueda, N. Kato, K. Hara, and K. Mizuno. LMNtal as a unifying declarative language: Live demonstration. In Proc. of ICLP'06. LNCS, 2006.