Abstract of Paper

On the Symbolic Analysis of Low-Level Cryptographic Primitives: Modular Exponentiation and the Diffie-Hellman Protocol
by Michele Boreale and Marzia Buscemi

Abstract:

Most of the automatic methods developed so far for analysis 
of security protocols model only a limited set of cryptographic 
primitives (often, only encryption and concatenation) and 
abstract from low-level features of cryptographic algorithms. 
This paper is an attempt to close this gap. We propose a 
symbolic technique for analysis of protocols based on modular 
exponentiation, such as Diffie-Hellman key exchange. We 
introduce a protocol description language along with its 
semantics. Then, we propose a notion of symbolic execution 
and, based on it, a verification method. We prove that the 
method is sound and complete with respect to the language 
semantics.