Verification of a Fair Non-Repudiation Protocol

Organisation:	CWI (THE NETHERLANDS) 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: http://homepages.cwi.nl/~dashti/icics.pdf or from the CADP Web site in PDF or PostScript
Contact:	Mohammad Torabi Dashti CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam THE NETHERLANDS Tel: +31 (0)20 592 4084 Fax: +31 (0)20 592 4199 Email: dashti@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page