Sciweavers

Share
CCS
2008
ACM

Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach

10 years 4 months ago
Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach
In the Horn theory based approach for cryptographic protocol analysis, cryptographic protocols and (Dolev-Yao) intruders are modeled by Horn theories and security analysis boils down to solving the derivation problem for Horn theories. This approach and the tools based on this approach, including ProVerif, have been very successful in the automatic analysis of cryptographic protocols w.r.t. an unbounded number of sessions. However, dealing with the algebraic properties of operators such as the exclusive OR (XOR) has been problematic. In particular, ProVerif cannot deal with XOR. In this paper, we show how to reduce the derivation problem for Horn theories with XOR to the XOR-free case. Our reduction works for an expressive class of Horn theories. A large class of intruder capabilities and protocols that employ the XOR operator can be modeled by these theories. Our reduction allows us to carry out protocol analysis by tools, such as ProVerif, that cannot deal with XOR, but are very eff...
Ralf Küsters, Tomasz Truderung
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CCS
Authors Ralf Küsters, Tomasz Truderung
Comments (0)
books