关键词: 模型检查, 协议验证, 认证协议, SPIN, EAPTLS

Abstract: 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.

Key words: model checking;protocol verification;authentication protocol;SPIN;EAPTLS