User Tools

Site Tools


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

@INPROCEEDINGS{Kuesters-CONCUR-2002,
  author      = {Ralf K{\"u}sters},
  title       = {{On the Decidability of Cryptographic Protocols with Open-ended Data Structures}},
  booktitle   = {13th International Conference on Concurrency Theory (CONCUR 2002)},
  year        = 2002,
  pages       = {515--530},
  publisher   = {Springer-Verlag},
  editor      = {L.~Brim and P.~Jancar and M.~Kretinsky and A.~Kucera},
  series      = {Lecture Notes in Computer Science},
  volume      = 2421,
  abstract    = {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.}
}