公平交换协议形式逻辑

• 作者: 吴中福 吴开贵 吴长泽 徐洁 陈明
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 异步通信 公平交换 形式化分析 推理逻辑 模型检查
• 年，卷（期）: 2011,（3）
• 页码范围: 509-521
• 分类号: TP309
• 字数: 12947字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.03945

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴中福	重庆大学计算机学院	194	2729	26.0	44.0
2	吴开贵	重庆大学计算机学院	57	699	12.0	24.0
3	吴长泽	重庆大学计算机学院	17	109	6.0	9.0
4	陈明	重庆大学计算机学院	15	80	7.0	8.0