Cryptographic protocol composition via the authentication tests

Abstract

Although cryptographic protocols are typically analyzed in isolation, they are used in combinations. If a protocol Π 1, when analyzed alone, was shown to meet some security goals, will it still meet those goals when executed together with a second protocol Π 2? Not necessarily: for every Π 1, some Π 2s undermine its goals. We use the strand space "authentication test" principles to suggest a criterion to ensure a Π 2 preserves Π 1's goals; this criterion strengthens previous proposals. Security goals for Π 1 are expressed in a language (Π 1) in classical logic. Strand spaces provide the models for (Π 1). Certain homomorphisms among models for (Π) preserve the truth of the security goals. This gives a way to extract-from a counterexample to a goal that uses both protocols-a counterexample using only the first protocol. This model-theoretic technique, using homomorphisms among models to prove results about a syntactically defined set of formulas, appears to be novel for protocol analysis. © 2009 Springer Berlin Heidelberg.