| On the Decidability of Cryptographic Protocols with Open-Ended Data Structures Ralf Kuesters 
      Formal analysis of cryptographic protocols has mainly concentrated on
      protocols with closed-ended data structures. That is, the messages
      exchanged between principals have fixed and finite format. However, in
      many protocols the data structures used are open-ended, i.e., messages
      have an unbounded number of data fields.  Formal analysis of protocols
      with open-ended data structures is one of the challenges pointed out
      by Meadows. This work studies decidability issues for such
      protocols. We propose a protocol model in which principals are
      described by transducers, i.e., finite automata with output, and show
      that in this model security - in presence of the standard Dolev-Yao
      intruder - is decidable and PSPACE-hard. | 
| concur02@fi.muni.cz |