Paper Info
Title
Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation
Abstract
ProVerif is one of the most successful tools for cryptographic protocol analysis. However, dealing with algebraic properties of operators such as the exclusive OR (XOR) and Diffie-Hellman exponentiation has been problematic. Recently, we have developed an approach which enables ProVerif, and related tools, to analyze a large class of protocols that employ the XOR operator. In this work, we adapt this approach to the case of Diffie-Hellman exponentiation. The core of our approach is to reduce the derivation problem for Horn theories modulo algebraic properties of Diffie-Hellman exponentiation to a purely syntactical derivation problem for Horn theories. The latter problem can then be solved by tools such as ProVerif.Our reduction works for a large class of Horn theories, allowing to model a wide range of intruder capabilities and protocols.We implemented our reduction and, in combination with ProVerif, applied it in the automatic analysis of several state-of-the-art protocols that use Diffie-Hellman exponentiation. While the general idea of our approach follows the one for XOR in our previous work, the reduction itself and the proof of soundness and completeness of our reduction are entirely different from the XOR case. Surprisingly, the reduction for Diffie-Hellman exponentiation is more efficient than the one for XOR.
Year
DOI
Venue
2009
10.1109/CSF.2009.17
CSF
Keywords
DocType
Citations 
latter problem,large class,diffie-hellman exponentiation,algebraic property,derivation problem,reduction work,xor operator,horn theory,syntactical derivation problem,xor case,analyze protocols,process algebra,exclusive or,diffie hellman,horn clauses,cryptographic protocols,data mining,computer security,cryptographic protocol,mathematical model,public key
Conference
39
PageRank 
References 
Authors
1.24
21
2
Name
Order
Citations
PageRank
Ralf Küsters1101469.62
Tomasz Truderung243917.37