Sciweavers

Share
STACS
2007
Springer

On the Automatic Analysis of Recursive Security Protocols with XOR

10 years 7 months ago
On the Automatic Analysis of Recursive Security Protocols with XOR
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.
Ralf Küsters, Tomasz Truderung
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where STACS
Authors Ralf Küsters, Tomasz Truderung
Comments (0)
books