Strand Spaces:
		     From Key Exchange Protocols
			  to Secure Location

			    Joshua Guttman
			     Vipin Swarup
			   F. Javier Thayer

			    The MITRE Corp.

Strand spaces are a special-purpose execution model for security
protocols, based on a Lamport-style causal partial ordering.
Behaviors of some principals, "regular principals," are assumed to
follow the rules of the protocol, while other, adversarial principals,
do whatever they like, constrained by cryptography and the secrets
they possess.  

The key notion is a possible global execution, or "bundle," namely a
causally well-founded directed acyclic graph, in which the nodes are
message transmissions or receptions.  The nodes may lie on any number
of regular or adversarial behaviors.  Every message reception must be
explained by some earlier transmission of the same message.  Causal
well-foundedness justifies a principle of induction for bundles, which
is the basis of powerful and reusable proof techniques.  Strand spaces
were intended to capture a minimal view of protocol behavior, leading
to conceptually spare and focused analysis techniques.

Secure location protocols combine cryptography with the physics of
message transmission.  The cryptographic operations authenticate the
principals and preserve confidentiality, while the physics of message
transmission constrain their possible locations.  We enrich the strand
space model by associating a space-time location with each node.  The
strands follow the world lines of principals.  Some bundles are
compatible with the physics of message transmission -- e.g. the
maximum message transmission speed -- while others are not.  An
assertion true in every bundle compatible with the physics is a valid
conclusion of a secure location protocol.

We will illustrate these ideas with some simple protocols.