Abstract: Strand space is a new model for the formal analysis of security protocols. By using the theory of order relation,
a very important conclusion used to analyze security protocols formally with the help of the strand space model is shown. By
constructing penetrator strands for the Woo-Lam protocol we present a strand space model infiltrated for this protocol.
Moreover, with the help of this strand space model infiltrated we analyze the flaw in this protocol and illustrate that this
flaw in this protocol can be overcome in the improved Woo-Lam protocol. The strand space model discussed above is
distinguished from other models by its simplicity and can avoid the state space explosion problem.

Key words: security protocol, formal analysis, strand space model, penetrator strand