Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security

Carlos Olarte (1) , Frank D. Valencia (1)

1 COMETE - Concurrency, Mobility and Transactions

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.

Mots clés: Concurrent Constraint Programming; Symbolic Semantics; Security; Mobility

Domaines: Logique en informatique [cs.LO]

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⟩