@inproceedings{8d40e66f51754c1ba87bd787b97b20db,
title = "Universal concurrent constraint programing: Symbolic semantics and applications to security",
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.",
keywords = "Concurrent constraint programming, Mobility, Security, Symbolic semantics",
author = "Carlos Olarte and Valencia, \{Frank D.\}",
year = "2008",
month = dec,
day = "1",
doi = "10.1145/1363686.1363726",
language = "English",
isbn = "9781595937537",
series = "Proceedings of the ACM Symposium on Applied Computing",
pages = "145--150",
booktitle = "Proceedings of the 23rd Annual ACM Symposium on Applied Computing, SAC'08",
note = "23rd Annual ACM Symposium on Applied Computing, SAC'08 ; Conference date: 16-03-2008 Through 20-03-2008",
}