Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation

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...

• Type: Conference
• Year: 2009
• Where: CSFW
• Authors: Ralf Küsters, Tomasz Truderung
• Keywords: Algebraic Properties, CSFW 2009, Diffie-Hellman Exponentiation, Horn Theories, Security Privacy