论文摘要
随着军队信息化建设进程的快速推进,来自内部实体的攻击严重威胁着军队的信息安全,非否认性和公平性主要解决的就是来自协议内部实体之间的攻击。然而长期以来,对密码协议安全特性的研究大部分集中在秘密性和认证性上,非否认性和公平性的研究是一个新兴的方向,目前还处于初级阶段。本文对非否认性和公平性的验证技术进行了探索,基于一阶逻辑提出了一种分析非否认性和公平性的新方法,并采用新方法成功地实现了对非否认协议的自动化验证。本文所做的工作主要包括以下几点:1.介绍了国内外现有的非否认性和公平性形式化分析方法,进行了分类比较,指出了每种方法的优缺点。2.针对非否认协议的特点提出了一套适用于描述和验证非否认性和公平性的一阶逻辑语法和语义。3.在语法和语义的基础上,提出了一种基于一阶逻辑建模非否认协议的方法,对模型中的各个要素分别进行了建模,给出了非否认性和公平性的一阶逻辑定义。这是本文工作的重点。4.用设计的模型对ZG非否认协议进行了手工推导,发现了协议的一个已知攻击,证明了模型的正确性、有效性以及模型的优点。5.根据模型,设计了相应的非否认性和公平性自动化验证算法,加入了必要的消解策略以减小算法复杂性、避免不可终止情况发生、提高算法效率。此部分是本文工作的难点。6.基于非否认协议的一阶逻辑模型及其验证算法,设计并开发了原型系统AVT-NR,简要介绍了系统的体系结构和工作流程,重点讨论了各部分的实现细节,并用该系统成功地分析了ZG非否认协议、ZG乐观非否认协议、KM非否认协议等非否认协议,进一步证明了新方法的有效性。