Computer Science – Cryptography and Security
Scientific paper
2008-08-05
Computer Science
Cryptography and Security
Scientific paper
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 efficient in the XOR-free case. We implemented our reduction and, in combination with ProVerif, applied it in the automatic analysis of several protocols that use the XOR operator. In one case, we found a new attack.
Kuesters Ralf
Truderung Tomasz
No associations
LandOfFree
Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-550253