Skip to Main content Skip to Navigation
Conference papers

Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security

Carlos Olarte 1 Frank D. Valencia 1
1 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 pi-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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00201497
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, December 30, 2007 - 9:19:57 PM
Last modification on : Thursday, March 5, 2020 - 6:18:35 PM
Long-term archiving on: : Thursday, September 27, 2012 - 1:30:24 PM

File

utccSac08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00201497, version 1

Collections

Citation

Carlos Olarte, Frank D. Valencia. Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security. 23rd Annual ACM Symposium on Applied Computing, ACM, Mar 2008, Fortaleza, Brazil. ⟨inria-00201497⟩

Share

Metrics

Record views

485

Files downloads

220