论文摘要
密码协议是在分布式网络环境中实现安全共享网络资源的基础，复杂的分布式网络环境使得攻击者可以利用密码协议的自身缺陷来实施各种攻击，从而达到破坏网络安全的目的，所以密码协议的安全性对于网络安全极为关键。密码协议的设计和分析是很困难，很容易出错的。尽管设计协议时考虑得非常周全，但协议设计出来后可能存在着漏洞，而且有些漏洞很隐蔽，很难被发现。因此密码协议设计和密码协议分析是信息安全领域的难题。密码协议分析早期采用非形式化方法，此类方法逐渐被更为严谨的形式化方法所取代。通常采用的形式化方法主要可分为信念逻辑、模型检测、定理证明技术等。 本文主要研究了一种较新的密码协议形式化方法—MSR(Multiset rewriting)模型。MSR用基于一阶原子公式的类型化的多重集重写规则描述协议动作，用存在量词模拟新鲜数的产生，是一种精确、灵活的密码协议形式化模型。本文所做的工作主要有以下几点： 1) 分析研究了基于多重集重写的MSR模型及相关理论。 2) 在MSR框架结构下定义了密码协议的秘密性和认证性。 3) 改进了协议模型和攻击者模型，主要解决了攻击者模型中出现的无限循环状态。 4) 用改进的MSR模型对NS密码协议和Zhou-Gollmann非否认协议进行了分析，证明了改进的MSR模型的合理性。 5) 学习了Maude语言，并对MSR原型工具进行了分析与改进，并用改进的工具分析验证了NS协议。