确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种，有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAPTLS进行验证,提取出包含协议设计重要细节的形式化模型，对协议安全属性采用线性时态逻辑抽象，并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。

It is important to guarantee the correctness of security protocols to ensure the securitysensitive businesses on the Internet. The formal method is useful to analyze and verify security protocols. It can uncover bugs which are difficult to find by testing. As a formalized method, model checking has many advantages. It is fully automatic, and also can provide faulty traces. An approach to abstracting and modeling the EAPTLS of 802.11i is presented by using model checker SPIN,and a formalized model of at a significant level of detail is extracted.The security properties of the protocol for verification are extracted using LTL to find if the security properties are true in the model. A way to model authentication protocols using PROMELA is presented.