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.
Category / Keywords: cryptographic protocols / Compositional protocol analysis, Dolev-Yao model, strand spaces Date: received 6 Oct 2008 Contact author: guttman at mitre org Available formats: PDF | BibTeX Citation Version: 20081008:154103 (All versions of this report) Discussion forum: Show discussion | Start new discussion