Database of Case Studies Achieved Using CADP

Verification of a Fair Non-Repudiation Protocol

University of Twente (THE NETHERLANDS)

Method: mCRL (micro Common Representation Language)
regular alternation-free mu-calculus

Tools used: CADP (Construction and Analysis of Distributed Processes)
mCRL toolset

Domain: Security protocols.

Period: 2005

Size: n/a

Description: A non-repudiation protocol is a security protocol, which provides evidence to sender and receiver agents that the sender has indeed sent a given message, and the receiver has indeed received it. In addition to secrecy and authentication, such a protocol must achieve fair exchange, which ensures that one of the agents does not get its evidence without the other one being able to get its one as well. Ensuring fair exchange properties is one of the major difficulties in designing non-repudiation protocols.

This case-study aims at verifying fair exchange properties on a new non-repudiation protocol proposed by the authors, which is simpler than existing ones. The protocol is specified in mCRL, and the properties, written in the regular alternation-free mu-calculus, are verified using CADP. The key of the verification is the use of a modified Dolev-Yao intruder, which ensures that messages sent over the network are eventually delivered.

Conclusions: The regular alternation-free mu-calculus is expressive enough to model fair exchange properties. CADP allowed to validate the protocol and to find vulnerabilities in a weaker version of the protocol.

Publications: [Cederquist-Corin-Dashti-05] J. Cederquist, R. Corin, and M.T. Dashti. "On the quest for impartiality: Design and analysis of a Fair Non-repudiation protocol". In Proceedings of the 7th International Conference on Information and Communications Security ICICS'2005 (Beijing, China), Lecture Notes in Computer Science, Vol. 3783, pp. 27-39, Springer Verlag, December 2005.
Available on-line at:
or from our FTP site in PDF or PostScript
Mohammad Torabi Dashti
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam
Tel: +31 (0)20 592 4084
Fax: +31 (0)20 592 4199

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page