首页 | 官方网站   微博 | 高级检索  
     

Z&G协议公平性的形式化验证
引用本文:龚德良,殷建平,詹宇斌.Z&G协议公平性的形式化验证[J].计算机科学,2008,35(9):76-82.
作者姓名:龚德良  殷建平  詹宇斌
作者单位:1. 汀南学院计算机科学系,郴州,423000
2. 国防科技大学计算机学院,长沙,410073
基金项目:国家自然科学基金,湖南省教育厅资助项目
摘    要:Zhou和Gollmann设计的公平非否认协议(Z&G协议)旨在为电子商务交易的双方提供非否认证据和公平性.提出一种基于状态转换的方法对其公平性进行分析.与以往方法不同,它是一种针对电子商务协议的专门分析工具:用状态转换系统为电子商务系统建模;用基于状态的形式系统描述协议,将协议的信任假设显式表示为协议的一部分.该方法按进程是否背离协议或者背离协议的程度将协议在系统中的执行序列定义为三类模式:遵守型、欺骗型和中断型.验证了Z&G协议在三种模式下的执行序列都满足公平性.

关 键 词:公平性  状态转换系统  遵守型  欺骗型  中断型

Analysis of Fairness of the Z&G Protocol
GONG De-liang,YIN Jian-ping,ZHAN Yu-bin.Analysis of Fairness of the Z&G Protocol[J].Computer Science,2008,35(9):76-82.
Authors:GONG De-liang  YIN Jian-ping  ZHAN Yu-bin
Affiliation:GONG De-liang1 YIN Jian-ping2 ZHAN Yu-bin2(Computer Science Department of Xiangnan College,Chenzhou 423000,China)1(School of Computer,National University of Defense Technology,Changsha 410073,China)2
Abstract:A non-repudiation protocol designed by Zhou and Gollmann is a typical electronic commerce protocol,which provides participants with fairness service.To verify the protocol this article models the electronic commerce system as the state transition system,specifies the protocol with state-based formalism,and formalizes fairness property in linear temporary logic.Protocol executions in the system are classified into three modes:compliance,deception and abortion,which have been analyzed and proved to satisfy fa...
Keywords:Fairness  Transition system  Compliance  Abortion  Deception  
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《计算机科学》浏览原始摘要信息
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司    京ICP备09084417号-23

京公网安备 11010802026262号