本文探讨了其它BAN类逻辑的缺陷及其产生原因，在此基础上提出了一种新的BAN类逻辑。 首先，本文探讨了BAN类逻辑的缺陷，并对产生缺陷的原因作了细致的分析，提出了作者自己独特的看法。 其次，本文首次阐释、构建了认证逻辑的理论基础。本文构造了一个带有二阶谓词的符号系统，在此基础上建立了一个二阶谓词逻辑公理系统，把该系统看作算术系统和集合论公理系统的扩充，并把认证逻辑看作该系统的一个特殊解释，从而把认证逻辑置于谓词逻辑这一坚实的理论基础之上。 第三，本文进一步澄清了语义。本文以几个十分简单清晰的命题为出发点，重新刻划了认证逻辑语义，其中不少命题都是本文首次提出的。 第四，本文提出了新的认证逻辑公理系统。本文给出了十八类共四十条公理。这些公理刻划了所使用的一阶谓词和二阶谓词的特点，并且说明了每个公理在“认证逻辑”这一解释下都是成立的，这使公理系统的可靠性得到了保证。 第五，本文对密码协议尤其是身份认证协议和密钥建立协议作了详细的分类，刻划了各类型协议的安全目标，并对协议安全性作了明确定义。本文对所定义的每一类型协议的安全目标都作了统一的公式化描述，进而以是否达到了相应目标为准则定义了协议的安全性。 第六，本文对若干常见密码协议进行了安全性分析。本文主要对身份认证协议和密钥建立协议进行了详细的分析，发现了许多协议是不安全的。此外还对电子选举协议、电子邮件协议和非否认协议等进行了分析，展示了本文的方法有着广泛的适用范围。 本文方法的最大特点是，克服了其它BAN类逻辑在分析协议时需要理想化过程的重大缺陷。