Analysis of Fairness of the Z&G Protocol
Z＆G协议公平性的形式化验证

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...