Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势. Strand Spaces is a machine verification method for analyzing security protocols. It briefly introduces the basic features of Strand Spaces, analyzes its advantages and disadvantages, and proposes an algorithm to construct the ideal sub-ring of the protocol, in order to restrict the protocol intruder’s Ability and number of protocols to run in parallel Combining model checking with Strand Spaces presents a synthetic approach to verifying protocol security features that takes advantage of both model checking and Strand Spaces.