Establishing and preventing a new replay attack on a non-repudiation protocol

Non-repudiation is a security service concerned with preventing a denial by one of the principals involved in a communication about having participated in this communication. In this paper, the Zhou Gollmann non-repudiation protocol is analyzed using an automated logic-based verification engine. As a result of this analysis a weakness in the protocol is discovered. Based on this weakness, a new replay attack on the Zhou Gollmann protocol is presented. In this attack, an intruder can incorrectly convince a principal to have successfully performed a new message exchange. As a consequence, the intruder can impersonate legitimate principals. The weakness leading to the attack is analyzed in detail and amendments to the protocol are proposed that prevent the presented attack. Further, formal verification of the amended protocol provides strong confidence in its correctness and effectiveness.