Automatic methods developed so far for analysis of security protocols only model 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 towards closing this gap. We propose a symbolic technique and a decision method 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.
Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation / M. BOREALE; M. G. BUSCEMI. - STAMPA. - (2003), pp. 269-278. [10.1007/978-3-540-45138-9_21]
Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation
BOREALE, MICHELE;
2003
Abstract
Automatic methods developed so far for analysis of security protocols only model 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 towards closing this gap. We propose a symbolic technique and a decision method 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.I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.