基于多智能体系统高效动态模型检测的大规模安全协议动态验证研究

安全协议是网络安全的基础，对协议进行安全性分析和验证是计算机安全领域发展前沿的重大课题之一，大规模安全协议验证是安全协议验证的难点。本项目的目标是研究基于多智能体系统高效动态模型检测的大规模安全协议动态验证方法和技术。具体包括四方面内容：(1) 提出基于时态认知信念逻辑体系，这种逻辑体系能更加准确地描述大规模安全协议的安全属性；（２）扩展并应用动态Bloom Filter　进行状态存储;研究规范自动机和系统自动机按需动态同步生成技术，提出有界动态同步模型检测理论和方法，以此为基础，形成大规模安全协议动态验证的方法和技术；（３）以所研究的方法和技术为基础，扩展NuSMV,开发大规模安全协议动态验证工具；（４）以上述方法、技术和验证工具为基础，对IPv4和IPv6等大规模安全协议进行安全性分析和验证。

安全协议是网络安全的基础，对协议进行安全性分析和验证是计算机安全领域发展前沿的重大课题之一，大规模安全协议验证是安全协议验证的难点。本项目的研究方向是基于外存的高效模型检测算法和大规模安全协议验证。经过三年的研究, 本项目共发表各类论文18篇, 其中SCI论文4篇,顶级会议论文2篇(AAAI-3013, IJCAI-2013), 有1篇SCI论文发表在影响因子超过4.1 的期刊上(Knowledge-Based Systems), 2篇SCI论文发表在国际顶级期刊(Artificial Intelligence)上。整个研究成果可以概况为以下四方面 (1) 建立了一套一阶时态认知信念逻辑体系，为大规模安全协议的属性描述提供了理论基础；(2) 系统研究并提出了一序列的基于外存的高效大规模系统模型检测技术，并以此为基础获得了大规模安全协议验证技术；(3) 基于模型检测工具SPIN, 开发了大规模系统模型检测软件和大规模安全协议验证工具；(4) 通过对标准大规模安全协议的验证与其他最具有代表性的国际先进模型检测工具进行对比, 显示了我们工具的优越性。