Paper Info
Title
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.
Year
DOI
Venue
2007
10.1007/978-3-540-70918-3_55
STACS
Keywords
Field
DocType
bounded number,recursive computation,recursive security protocol,certain assumption,existing decision procedure,protocols recursive protocol,recursive protocol,security relevant property,certain horn theory,security protocol,group protocol,automatic analysis
Combinatorics,Algebraic number,Cryptographic protocol,Computer science,Exclusive or,Theoretical computer science,Decidability,Operator (computer programming),Recursion,Computation,Bounded function
Conference
Volume
ISSN
Citations 
4393
0302-9743
13
PageRank 
References 
Authors
0.63
14
2
Name
Order
Citations
PageRank
Ralf Küsters1101469.62
Tomasz Truderung243917.37