主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
陈明,吴开贵,吴长泽,徐洁,吴中福.公平交换协议形式逻辑.软件学报,2011,22(3):509-521
公平交换协议形式逻辑
Formal Logic for Fair Exchange Protocols
投稿时间:2009-11-05  修订日期:2010-09-06
DOI:10.3724/SP.J.1001.2011.03945
中文关键词:  异步通信  公平交换  形式化分析  推理逻辑  模型检查
英文关键词:asynchronous communication  fair exchange  formalize analysis  logical reasoning  model checking
基金项目:国家自然科学基金(90818028); 国家科技支撑计划(2008BAH37B04)
作者单位E-mail
陈明 重庆大学 计算机学院,重庆 400044 chenming9824@yahoo.com.cn 
吴开贵 重庆大学 计算机学院,重庆 400044  
吴长泽 重庆大学 计算机学院,重庆 400044  
徐洁 重庆大学 计算机学院,重庆 400044
School of Computing, University of Leeds, UK 
 
吴中福 重庆大学 计算机学院,重庆 400044  
摘要点击次数: 3773
全文下载次数: 3743
中文摘要:
      在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke 结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.
英文摘要:
      The fairness and punctuality of optimistic fair exchange protocols are difficult to analyze by using belief logic. Based on the studies of existing formal models and security attributes in fair exchange, a formal model for logic reasoning and fair exchange protocols is proposed. In the model, the channel errors are transferred to the attacker’s behaviors, the participants are divided into honest and dishonest ones, and the threats are attributed to two types of intruders. Based on the idea of model checking, the protocols are defined as an evolved system that has the Kripke structure, and the parties are considered as processes in an asynchronous environment. The new logic stimulates the time operators to control the transfers among the participants’ behaviors and is simple and easy to use. Through typical optimistic fair exchange protocols, the article demonstrates the course of protocol analysis. Two flaws of the protocol are discovered and improved. The case study shows that the new logic can be used to analyze the fairness and timeliness of fair exchange protocols.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利