安全协议为网络信息交换提供安全服务,是保证网络安全的基础。但攻击者可利用安全协议自身的缺陷来实施各种各样的攻击,因此安全协议的安全性成为网络安全的关键。早期人工证明的协议分析方式极易出错,其检测的范围也过于狭窄。由于安全协议目标的微妙性、协议运行环境的复杂性、攻击的多样性以及协议运行的高并发性,迫切需要研究和设计更可靠的安全协议形式化分析方法。本文提出一种新的安全协议的形式化验证逻辑,在协议分析的两个重要方面——协议的形式化和攻击模型的设计都作出了改进。该形式化方法有效克服了基于信仰的逻辑证明方法的不足,不仅可找到攻击,也可证明协议的安全性。本文还提出一种扩充的入侵模型,模型中应用了术语猜测和Hash碰撞理论。其中术语猜测是近年来协议分析的研究新热点。Hash碰撞是密码学方面的最新重大突破,据此本文首次提出Hash伪造攻击。基于这种扩充,本文的方法找到了更多新的协议攻击。在此基础上,本文针对如何有效避免这些新型攻击给出协议修改建议。同时本文分析了两种重要协议——电子商务协议和安全套接层协议的安全性。最后本文实现了基于本文验证逻辑和入侵模型的协议自动化分析系统,设计了用于实现自动化分析的协议说明语言,首次提出将协议说明语言分层实现的设计思想。与已有的自动化分析工具相比,该系统可分析的协议类型更广泛,得出的攻击更全面,并且对协议安全性的证明更可信。根据作者检索结果,目前尚无其他自动化工具发现Woo-LamΠ4的猜测攻击和MS-CHAPv2的Hash伪造攻击。本文的研究对安全协议的验证和设计乃至电子商务、军事、无线通信等网络安全研究具有一定参考价值。