认证协议是在移动通信网和计算机网络中采取的一个重要的安全措施。一个安全的认证协议能有效抵御恶意的攻击者对通信网进行的欺诈，保证通信网的安全运行。在不同的环境下如何设计正确的认证协议是一个值得研究的题目，这包括协议的设计过程和分析过程。在分析认证协议的工具中，形式分析以其客观性、准确性占有重要的地位。而在形式分析中，BAN逻辑以其简单性和有效性得到了普遍的应用和广泛的研究。本论文从分析和设计的角度对认证协议进行了研究，所做的工作有以下几点：●研究了Wenbo Mao提出的类BAN逻辑，指出由于在逻辑中引入“认证主体看 不到的”逻辑概念，而没有相应的语义来支持，导致了其逻辑存在着模糊性， 通过实例说明了其局限性。●完善了利用随机数和认证主体级连的协议理想化N-u方法。●提出了一种扩展的BAN逻辑，此扩展的逻辑适用于公钥密码体制认证协议的 形式分析。●提出了利用BAN逻辑设计认证协议的5条准则，和相应的符合BAN逻辑的 基本信息结构，并利用基本信息结构设计了一个认证协议。●用形式分析的方法分析了移动通信中的认证协议，指出Beller-Yacobi协议是一 个设计比较完善的协议。利用“一次性证书”设计了移动通信中的协议，并用 形式分析的方法证明了其正确性。●研究了移动通信中的匿名问题，设计了一个对访问域和其他移动用户具有匿名 功能的认证协议。