The inductive approach to strand space

Abstract

Strand space is a promising technique developed by Guttman et al. from MITRE company, and it provides us an intuitive and clear framework to analyze security protocols, but its mechanics of the proof tend to be quite intricate and not necessarily easy to be formalized. In this paper, we combine the inductive approach with strand space. We introduce an inductive definition for bundles, and it not only provides us a constructive illustration for a bundle, but also introduces an effective and rigorous technique of rule induction to prove properties of bundles. Using this induction principle, we not only prove that a bundle is a casually well-founded graph, but also give a rigorous proof for results of authentication tests. Our result of authentication test extends Guttman's result to a more general case, and its proof is also much easier and clearer. As a trivial case study, we prove authentication properties of Needham-Schroeder-Lowe protocol. Our approach has been mechanized using Isabelle/HOL. © IFIP International Federation for Information Processing 2005.