随着信息技术的快速发展和广泛应用,诸如电子商务这类需要高度安全性的应用逐渐普及,建立安全信道的重要性可想而知。在网络这个特殊的大环境里,两个互相不认识的主体如果想要达成某种通信目的,必须要在密码技术保障的前提下进行。虽然现阶段对密码协议的分析方法的研究已经有了很多观点,但是还没有一种被广泛认同的可以作为工业标准的方法,所以对于密码协议的形式化分析方法仍然是一个开放性的热点问题,而且具有重要的理论意义。本文首先介绍了密码学领域的一些基本概念,密码协议的分类,以及在密码协议中需要用到的一些重要的密码学技术:保密性,数据完整性,抗抵赖性以及消息认证性。为了使得分析方法的设计更加具有针对性,本文假设所讨论的协议都是在底层密码技术安全的前提下进行的;然后,本文通过分析密码协议形式化方法的主流观点,总结出这些观点存在的缺陷。接着通过对一些经典的攻击方式的分析,引出本文的主题,即对密码协议安全性分析的形式化方法,提出这套方法的依据在于Bellare和Rogaway对于密码协议安全的公式化定义,以及作者在学习过程中总结出的一些密码协议的设计原则。这个形式化方法分为五个模块,首先对协议进行前四个模块的检验,然后在第五个模块中对协议进行安全性证明。本文通过对大量相关文献的研究,深深的体会到对于密码协议安全性证明的困难性。所以本文所采用的证明方式基于不同于传统密码学证明的逻辑方式,并不是将攻击者攻破协议的行为归约到攻破数学难题上,而是归约到对已知假设的否定上,每个步骤在逻辑上都严密合理。接下来利用这套方法对一些工业协议例如SSH,Kerberos以及STS协议进行分析;最后,对密码协议的研究做出总结和展望。