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

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

项目编号： No.61163001

项目类型： 地区科学基金项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 龙士工

作者单位： 贵州大学

项目金额： 36万元

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

中文关键词： 行为时序逻辑；模型检测；公平性；协议分析；

英文摘要：

英文关键词： TLA；Model checking；fairness；protocol analysis；