Mobile Calculi based on Domains


Symbolic analysis of crypto-protocols based on modular exponentiation

M. Boreale and M. Buscemi

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.

@InProceedings\{boreale.buscemi:symbolic-analysis-crypto-protocols,
  author = \{M. Boreale and M. Buscemi},
  title = \{Symbolic analysis of crypto-protocols based on modular exponentiation},
  booktitle = \{Proc. of MFCS 2003},
  year = \{2003}, 
  volume = \{2747}, 
  series = \{Lecture Notes in Computer Science}, 
  publisher = \{Springer}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi_symbolic-analysis-crypto-protocols.pdf}
}


About this site. Last modified: Wed Nov 22 08:35:03 CET 2017