Z＆G协议公平性的形式化验证

计算机科学 ›› 2008, Vol. 35 ›› Issue (9): 76-82.

Z＆G协议公平性的形式化验证

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
国家自然科学基金（60473057）和湖南省教育厅重点科研基金（2006A006）资助.

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： Zhou和Gollmann设计的公平非否认协议（Z＆G协议）旨在为电子商务交易的双方提供非否认证据和公平性。提出一种基于状态转换的方法对其公平性进行分析。与以往方法不同，它是一种针对电子商务协议的专门分析工具：用状态转换系统为电子商务系统建模；用基于状态的形式系统描述协议，将协议的信任假设显式表示为协议的一部分。该方法按进程是否背离协议或者背离协议的程度将协议在系统中的执行序列定义为三类模式：遵守型、欺骗型和中断型。验证了Z＆G协议在三种模式下的执行序列都满足公平性。

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

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

Key words: Fairness,Transition system,Compliance,Abortion,Deception

. Z＆G协议公平性的形式化验证[J]. 计算机科学, 2008, 35(9): 76-82. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed