Cryptographic Protocol Composition via the Authentication Tests

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(Π) in classical logic describes executions of a protocol Π, and expresses its security goals. Strand spaces provide the models for L(Π). Second, the strand space “authentication test” principles suggest our syntactic criterion for security goals to be preserved. Third, certain homomorphisms among models for L(Π) 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 ...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Joshua D. Guttman
• Keywords: Applied Computing, FOSSACS 2009, Security Goals, Strand Space, Syntactic Criteria