密码学的中心任务之一就是设计密码协议, 密码协议是通讯和网络安全体系,分布式系统和电子商务的关键组成部分和主要保障手段和工具.本项目是为了克服现在密码协议分析形式化方法的不完全不可靠的缺点, 弥补可证安全分析的复杂和难以操作的缺点. 通过研究总结出集多种方法优点于一体的形式化模型, 并在其中引入计算复杂性的概念和手段,建立安全分析的方法.项目将通过三个过程达到目标: 1. 甄选出一种形式简明,表达力强,具有大多数模型优点的形式化模型. 并具有可扩展性, 以适应与可证安全方法的融合. 2. 研究在可证安全方法中如何放松对于理想模型下实现现实协议的要求,并能够保持复合的性质. 3. 以此为基础, 与模型检测的模型相结合, 形成安全可靠的易于操作的密码协议分析模型.该方法的形成将为协议设计和分析提供有力的工具,对于密码学的发展起到积极的促进作用.
本项目对目前的形式化方法进行归纳、分析和总结,比较了各种流行的模型的优缺点。 特别是对于Strand Space 模型进行了归纳总结。对于该模型投入力量进行了扩充。并且利用该模型的扩充成功的对于现行的协议进行分析。分析了一些新的密码协议和方案,发现了一些缺陷和漏洞, 并提出改进方案。 对于可证安全的协议分析方法进行了探讨,发表了一些基本结果。主要表现在对于零知识集合以及利用零知识集合对于安全协议的分析和安全性证明。在前面研究工作的基础上,我们提出了一种新的形式化分析协议的语义模型。这个方法的特点是,具有方便自然,灵活的优点。利用该模型我们对于具体的协议进行了分析。但是我们在研究过程中发现,将现有的可证明安全的思想方法与目前的现实化方法结合是一个很大的挑战,具有一定的难度。我们及时地调整了项目的目标,在继续沿着项目目标研进的同时,着力于利用现有的模型方法对于具体的协议进行分析,以及构造新的安全协议的方案。项目取得了丰富的成果,共发表论文39篇,并汇编安全协议研讨会论文集一部。论文中有6篇国际SCI,9篇EI,ISTP 会议论文11 篇。