公平交换协议形式逻辑

摘要：

在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.

关键词：异步通信、公平交换、形式化分析、推理逻辑、模型检查

所属期刊栏目：22

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金90818028;国家科技支撑计划2008BAH37B04

在线出版日期：2011-05-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共13页

页码：509-521