Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security - Archive ouverte HAL Access content directly
Conference Papers Year : 2008

Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security

(1) , (1)
1
Carlos Olarte
  • Function : Author
  • PersonId : 845696
Frank D. Valencia
  • Function : Author
  • PersonId : 845697

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.
Fichier principal
Vignette du fichier
utccSac08.pdf (182.67 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00201497 , version 1 (30-12-2007)

Identifiers

  • HAL Id : inria-00201497 , version 1

Cite

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⟩
186 View
125 Download

Share

Gmail Facebook Twitter LinkedIn More