Workshop on
Foundations of Computer Security - FCS'03
Ottawa, Canada, 26-27 June 2003
On the Symbolic Analysis of Low-Level Cryptographic Primitives:
Modular Exponentiation and the Diffie-Hellman Protocol
Michele Boreale (University of Firenze - Italy) and Marzia Buscemi
(University of Pisa - Italy)
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.