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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Boreale, M., & Buscemi, M. G. (2003). Symbolic analysis of crypto-protocols based on modular exponentiation. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2747, 269–278. https://doi.org/10.1007/978-3-540-45138-9_21
Mendeley helps you to discover research relevant for your work.