User Tools

Site Tools

On the Automatic Analysis of Recursive Security Protocols with XOR (BibTeX)

  author      = {Ralf K{\"u}sters and Tomasz Truderung},
  title       = {{On the Automatic Analysis of Recursive Security Protocols with XOR}},
  booktitle   = {Proceedings of the 24th Symposium on Theoretical Aspects of Computer Science (STACS 2007)},
  pages       = {646--657},
  editor      = {W.~Thomas and P.~Weil},
  year        = 2007,
  volume      = 4393,
  series      = {Lecture Notes in Computer Science},
  publisher   = {Springer},
  abstract    = {In many security protocols, such as group protocols, principals have to perform iterative or recursive computations. We call such protocols recursive protocols. Recently, first results on the decidability of the security of such protocols have been obtained. While recursive protocols often employ operators with algebraic, security relevant properties, such as the exclusive OR (XOR), the existing decision procedures, however, cannot deal with such operators and their properties. In this paper, we show that the security of recursive protocols with XOR is decidable (w.r.t.~a bounded number of sessions) for a class of protocols in which recursive computations of principals are modeled by certain Horn theories. Interestingly, this result can be obtained by a reduction to the case without XOR.  We also show that relaxing certain assumptions of our model lead to undecidability.}