| 公平交换协议形式逻辑 |
| |
| 引用本文： | 陈明,吴开贵,吴长泽,徐洁,吴中福.公平交换协议形式逻辑[J].软件学报,2011,22(3):509-521. |
| |
| 作者姓名： | 陈明 吴开贵 吴长泽 徐洁 吴中福 |
| |
| 作者单位： | 1. 重庆大学计算机学院,重庆,400044
2. 重庆大学计算机学院,重庆,400044;School of Computing,University of Leeds,UK |
| |
| 基金项目： | 国家自然科学基金(90818028); 国家科技支撑计划(2008BAH37B04) |
| |
| 摘 要： | 在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.
|
| 关 键 词： | 异步通信 公平交换 形式化分析 推理逻辑 模型检查 |
| 收稿时间： | 2009/11/5 0:00:00 |
| 修稿时间： | 9/6/2010 12:00:00 AM |
Formal Logic for Fair Exchange Protocols |
| |
| CHEN Ming,WU Kai-Gui,WU Chang-Ze,XU Jie and WU Zhong-Fu.Formal Logic for Fair Exchange Protocols[J].Journal of Software,2011,22(3):509-521. |
| |
| Authors: | CHEN Ming WU Kai-Gui WU Chang-Ze XU Jie and WU Zhong-Fu |
| |
| Affiliation: | College of Computer Science, Chongqing University, Chongqing 400044, China;College of Computer Science, Chongqing University, Chongqing 400044, China;College of Computer Science, Chongqing University, Chongqing 400044, China;College of Computer Science, Chongqing University, Chongqing 400044, China; School of Computing, University of Leeds, UK;College of Computer Science, Chongqing University, Chongqing 400044, China |
| |
| Abstract: | |
| |
| Keywords: | asynchronous communication fair exchange formalize analysis logical reasoning model checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
