Welcome to the resource topic for 2008/430
Title:
Cryptographic Protocol Composition via the Authentication Tests
Authors: 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.
ePrint: https://eprint.iacr.org/2008/430
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .