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},
  institution = {ETH Zurich},
  year        = 2007,
  note        = {An abridged version appears in STACS 2007},
  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.}