中文摘要：

串空间是安全协议形式化分析的一种新模型．利用次序关系的理论证明了借助串空间模型进行安全协议形式化分析的一个重要结论．通过构造入侵者串的方法．针对Woo-Lam协议提出了一个入侵者串空间模型．同时利用此入侵者串空间模型分析了该协议存在的缺陷．说明了改进后的Woo-Lam协议可克服此缺陷．与现有安全协议形式化分析方法相比较．串空间模型不仅具有简洁直观的优点，而且还可避免状态空间爆炸的问题．

英文摘要：

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.