Formal Analysis of a Non-Repudiation Protocol

This paper applies the theory of Communicating Sequential Processes (CSP) to the modelling and analysis of a non-repudiation protocol. Non-repudiation protocols differ from authentication and key-exchange protocols in that the participants require protection from each other, rather than from an external hostile agent. This means that the kinds of properties that are required of such a protocol, and the way it needs to be modelled to enable analysis, are different to the standard approaches taken to the more widely studied class of protocols and properties. A non-repudiation protocol proposed by Zhou and Gollmann is analysed within this framework, and this highlights some novel considerations that are required for this kind of protocol. 1. Introduction Over the past few years, formal methods have been successfully applied to the analysis of security protocols. The bulk of the effort has been concerned with authentication and confidentiality properties, and there are now a range of matu..