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 ∏_2 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.rnSecurity goals for ∏_1 are expressed in a language L(∏_1) in classical logic. Strand spaces provide the models for L(∏_1). Certain homo morphisms among models for L(∏) 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.
展开▼
