Automatically Analysing Non-repudiation with Authentication

Non-repudiation protocols must ensure that when two parties exchange informations over a network, neither one nor the other can deny having participated in this communication. While security issues such as secrecy and authentication have been studied intensively, interest in non-repudiation has only come in recent years and most of the non-repudiation protocol analysis has been done manually. In this paper we present how non-repudiation properties can be modeled as authentication properties; the AVISPA Tool, that supports secrecy and authentication only, is used to automatically analyse the non-repudiation properties of the Fair Zhou-Gollmann protocol.