User Tools

Site Tools


On the Decidability of Cryptographic Protocols with Open-ended Data Structures (BibTeX)

@ARTICLE{Kuesters-IJIS-2004,
  author = {Ralf K{\"u}sters},
  title = {{On the Decidability of Cryptographic Protocols with Open-ended Data Structures}},
  journal = {International Journal of Information Security},
  year = 2005,
  volume = 4,
  number = {1--2},
  pages = {49--70},
  note = {Online publication appeared 2004. DOI: 10.1007/s10207-004-0050-z.},
  abstract = {Formal analysis of cryptographic protocols has mainly concentrated on protocols with closed-ended data structures, i.e., protocols where the messages exchanged between principals have fixed and finite format. In many protocols, however, the data structures used are open-ended, i.e., messages have an unbounded number of data fields.  In this paper, decidability issues for such protocols are studied. 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 is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.}
}