User Tools

Site Tools


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

@TECHREPORT{Kuesters-IFI-0204,
  author = {Ralf K{\"u}sters},
  title = {{On the Decidability of Cryptographic Protocols with Open-ended Data Structures}},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik, CAU Kiel, Germany},
  year = 2002,
  number = {0204},
  note = {Available from \url{http://www.informatik.uni-kiel.de/ifi/forschung/technische-berichte/}},
  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.  This work studies decidability issues for protocols with open-ended data structures.  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. }
}