随着Internet技术的发展,安全协议在电子商务和电子政务中的应用越来越多。与此相应的就是人们对协议的安全性更加关注,尤其是在特殊环境下如何建模和分析安全协议显得尤为重要。本文首先研究和分析了现有的安全协议的建模和分析方法,找出其中的优势和不足。考虑环境的特殊性,选用符合标准的基于事件的GSPML语言对广义的挑战-应答协议和TLS握手协议的简化版本建立了可视化的模型。在此基础上,本文对广义的挑战-应答协议的安全条件进行了分析,列出了在对称密码体制和非对称密码体制下挑战-应答协议需要满足的安全条件,以及不满足这些条件将会导致的攻击和与之相应的协议认证性的缺失。值得注意的是,在两种密码体制下挑战-应答协议在最小形式上是有所区别的。然后,作者对传统认为的三轮认证协议进行了分析,认为在有主动攻击者存在的情况下,单纯的认证协议无法完全保证认证的目的。此外,本文对四种形式化方法的自动工具进行了分析,这些工具涵盖了形式化分析方法的三大流派。作者主要从用户界面和易用性,运行状态数和时间,数据独立性和离散时间支持,协议错误的发现能力这四个方面进行比较,并给出了综合能力的结论。