Analyzing the Zhou-Gollmann Non-Repudiation Protocol

Non-repudiation protocols are concerned with preventing a principal to deny having been involved in some communication. This paper reviews and analyses the Zhou Gollmann non–repudiation protocol using an automated logic-based verification engine. The formal verification of the protocol is presented and the results are discussed. The investigations reveal the presence of a freshness weakness in the protocol. A new attack on the protocol that exploits this weakness is presented and analyzed. This attack allows an intruder to impersonate legitimate principals by using previously recorded messages. As a consequence of this attack, a honest principal is led to believe to have performed multiple instances of the protocol, whereas in fact only one genuine protocol run has taken place.