Formal Analysis and Improvement of ZG Non-repudiation Protocol

A non-repudiation protocol aims to provide non-repudiation service. Non-repudiation service, one of the essential security services in computer networks, protects the parties involved in a transaction against the other party denying that a particular event or action took place. Non-repudiation protocols are a special type of fair exchange protocols, and fairness is a key property that must be respected in non-repudiation. Zhou and Gollmann proposed two well-known non-repudiation protocols, one with an online-TTP (ZG online) and the other with an offline-TTP (ZG offline). Both non-repudiation protocols were extensively analyzed in literature, but the ZG offline protocol was widely regarded as secure, that is, satisfying the properties of fairness. In this paper, however, using a formal method based on the strand space theory, we analyzed the ZG offline protocol and found a weakness that may endanger the fairness of the protocol. An improvement of the protocol was proposed and formally analyzed.