Paper 2008/430

Cryptographic Protocol Composition via the Authentication Tests

Joshua D. Guttman

Abstract

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.