Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security

Carlos Olarte 1 Frank D. Valencia 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Type de document :
Communication dans un congrès
23rd Annual ACM Symposium on Applied Computing, Mar 2008, Fortaleza, Brazil. 2008
Liste complète des métadonnées

https://hal.inria.fr/inria-00201497
Contributeur : Catuscia Palamidessi <>
Soumis le : dimanche 30 décembre 2007 - 21:19:57
Dernière modification le : mercredi 14 novembre 2018 - 16:10:03
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:30:24

Fichier

utccSac08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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, Mar 2008, Fortaleza, Brazil. 2008. 〈inria-00201497〉

Partager

Métriques

Consultations de la notice

434

Téléchargements de fichiers

179