安全协议的行为时序逻辑验证与具有公平性约束的部分状态空间模型检测

安全协议是建立在密码体制基础上的一种交互通信协议。尽管许多安全协议经过精心设计，但仍然可能存在安全漏洞,借助于形式化分析方法对安全协议进行分析和验证则成为一种必然的趋势。 行为时序逻辑TLA是由美国科学家Leslie Lamport提出的一种组合了时序逻辑与行为逻辑的程序逻辑，用于对并发系统进行描述和验证。具体内容有：(1)扩展TLA的理论，扩展和补充一些重要的密码学和信息传递的重要谓词，提出新的逻辑公式推演方法，尽量减少初始化假设引入；(2）研究TLA逻辑公式在推演系统中的形式可推演性、形式可证明性、协调性，以及极大协调性,增加新的推演规则，以适应对对安全协议形式化分析的需要；(3)研究高效的基于TLA的部分状态空间模型检测算法，主要是通过公平性约束条件，并通过定义满足序关系的部分状态空间结构，从而达到有助于减少状态空间的目的。

项目围绕以行为时序逻辑和模型检测简化算法为核心的一些关键问题展开研究；扩展了行为时序逻辑的语法功能；为了解决模型检测空间爆炸问题，研究了模型检测的简约算法，并以行为时序逻辑为基础，展开了若干模型检测方面的应用；设计了一个模型检测基础平台。具体包括：1、对行为时序逻辑进行了扩充，提出了概率行为时序逻辑，通过在原有逻辑基础上增加概率行为属性和概率操作符的方法，扩充了原有的逻辑，利用扩充的概率行为逻辑可以描述概率系统及验证概率性质；2、基于行为时序逻辑语义证明方法，证明行为时序逻辑的弱公平性的活性规则和强公平性的活性规则；3、利用偏序规约解决状态爆炸问题的方法；即为了论证属性是否满足系统，仅仅探测全状态空间约简部分即可；4、利用充足集、持久集和顽固集，设计和分析状态空间搜索算法，在每个状态搜索中，仅仅搜索在当前状态变迁关系集合的一个子集；5、设计了基于睡眠集的空间搜索算法，利用睡眠集概念，可以剔除每个状态上在睡眠集中使能但没有必要执行的转换，从而可以简化状态空间。6、针对模型检测复杂系统空间爆炸问题，研究并提出了分解策略，将复杂系统分解成组件，利用组件之间的逻辑接口进行输入和输出操作，通过TLA+对各个组件抽象建模，并通过模型检测工具TLC验证各个组件的安全性和活性，有效克服了空间爆炸问题，实现了对复杂系统的模型检测。7、设计并实现了一个模型检测的基础平台，在该平台上完成了包括协议分析、算法分析以及NP问题计算计算的各种应用，并得到了一些实验结果。. 项目组在行为时序逻辑和模型检测的理论、方法和应用上有了一定的突破和创新，圆满完成了项目计划任务和目标，在科学研究、人才培养和团队建设方面取得了较好的效果。