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

关键词：模型检查 协议验证 认证协议 spin eap 

单位：湖南大学软件学院 湖南长沙410082