Cryptographic Protocol Composition via the Authentication Tests Joshua D. Guttman The MITRE Corporation Monday, February 23, 2009 11:00 a.m. - 12:00 p.m. Fuller Labs, Perreault Hall Although cryptographic protocols are typically analyzed in isolation, they are used in combinations. If a protocol Pi_1, when analyzed alone, was shown to meet some security goals, will it still meet those goals when executed together with a second protocol Pi_2? Not necessarily: for every Pi_1, some Pi_2s undermine its goals. We use the strand space ``authentication test'' principles to suggest a criterion to ensure a Pi_2 preserves Pi_1's goals; this criterion strengthens previous proposals. Security goals for Pi_1 are expressed in a language L(Pi_1) in classical logic. Strand spaces provide the models for L(Pi_1). Certain homomorphisms among models for L(Pi) 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 momorphisms among models to prove results about a syntactically defined set of formulas, appears to be novel for protocol analysis. Appears in: Foundations of Software Science and Computation Structures, ETAPS, March 2009. LNCS 5504. Paper available at: http://www.dcs.qmul.ac.uk/~joshuag/pubs/fossacs_disjoint.pdf ______ Host: Michael Gennert Refreshments will be served. Maintained by webmaster@cs.wpi.edu Last modified February 18.,2009

Department of Computer Science - Worcester Polytechnic Institute
100 Institute Road, Worcester, MA 01609-2280
Phone: +1-508-831-5357 - Fax: +1-508-831-5776 - cs@wpi.edu