Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols

Hubert Comon7, 8 Contact Information, Véronique CortierContact Information and John MitchellContact Information

(7)  Department of Computer Science, Stanford University, Gates 4B, CA, 94305-9045
(8)  Laboratoire Spécification et Vérification, CNRS and Ecole Normale Supérieure de Cachan, France
Abstract
We introduce a class of tree automata that perform tests on a memory that is updated using function symbol application and projection. The language emptiness problem for this class of tree automata is shown to be in DEXPTIME. We also introduce a class of set constraints with equality tests and prove its decidability by completion techniques and a reduction to tree automata with one memory. Set constraints with equality tests may be used to decide secrecy for a class of cryptographic protocols that properly contains a class of memoryless “ping-pong protocols” introduced by Dolev and Yao.
Partially supported by DoD MURI “Semantic Consistency in Information Exchange,” ONR Grant N00014-97-1-0505, and NSF CCR-9629754.

Contact Information Hubert Comon
Email: comon@theory.stanford.edu
Email: comon@lsv.ens-cachan.fr

Contact Information Véronique Cortier
Email: cortier@lsv.ens-cachan.fr

Contact Information John Mitchell
Email: jcm@theory.stanford.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb02
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)