CWI (THE NETHERLANDS)
University of Twente (THE NETHERLANDS)
mCRL (micro Common Representation Language)
regular alternation-free mu-calculus
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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,
Available on-line at: http://homepages.cwi.nl/~dashti/icics.pdf
or from the CADP Web 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: http://cadp.inria.fr/case-studies|