Paper 2008/430

Cryptographic Protocol Composition via the Authentication Tests

Joshua D. Guttman


Although cryptographic protocols are typically analyzed in isolation, they are used in combinations. If a protocol was analyzed alone and shown to meet some security goals, will it still meet those goals when executed together with a second protocol? While not every choice of a second protocol can preserve the goals, there are syntactic criteria for the second protocol that ensure they will be preserved. Our main result strengthens previously known criteria. Our method has three main elements. First, a language L(\Pi) in classical logic describes executions of each protocol \Pi, and expresses its security goals. Strand spaces provide the models for L(\Pi). Second, the strand space ``authentication test'' principles suggest our syntactic criterion for security goals to be preserved. Third, certain homomorphisms among models for L(\Pi) preserve the truth of formulas of the syntactic form that security goals take. This provides a way to extract -- from a counterexample to a goal that uses both protocols -- a counterexample using only the first protocol. This essentially model-theoretic technique studies a syntactically defined set of formulas using the homomorphisms among their models. It appears to be novel for protocol analysis.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Compositional protocol analysisDolev-Yao modelstrand spaces
Contact author(s)
guttman @ mitre org
2008-10-08: received
Short URL
Creative Commons Attribution


      author = {Joshua D.  Guttman},
      title = {Cryptographic Protocol Composition via the Authentication Tests},
      howpublished = {Cryptology ePrint Archive, Paper 2008/430},
      year = {2008},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.