CWI (THE NETHERLANDS)
mCRL (micro Common Representation Language)
regular alternation-free mu-calculus
CADP (Construction and Analysis of Distributed Processes)
(distributed) mCRL toolset
This case study is about the formal verification of a fair exchange
protocol using a finite state model-checker. An exchange protocol
involves two parties, A and B. When the protocol starts,
each party has an item that it wants to exchange with the other party.
An exchange protocol is called fair if, when it has terminated,
either A has received B's item and B has received
A's item, or none of the parties has lost its item. Notice that
the expression of fairness properties involves liveness properties,
unlike the classical view of security, which uses only safety
The protocol is specified using mCRL, including an extension of the Dolev-Yao intruder. This extension is needed to take into account that fairness requires resilient communication channels, i.e., all messages sent should eventually be delivered.
Using the model checker EVALUATOR of CADP, not only fairness, but also other properties of the protocol, such as correctness, effectiveness, and timeliness, have been verified.
This case study shows that the finite state model checker EVALUATOR of
CADP can be easily used to help finding flaws in a security protocol.
Jan G. Cederquist and Muhammad Torabi Dashti.
"Formal Analysis of a Fair Payment Protocol". In Formal Aspects in
Security and Trust, Proceedings of the IFIP TC1 WG1.7 Workshop on
Formal Aspects in Security and Trust FAST'2004 (Toulouse, France),
Kluwer Academic Publishers, August 2004.
Preliminary version available on-line at: http://www.cwi.nl/ftp/CWIreports/SEN/SEN-R0410.pdf
or from the CADP Web site in PDF or PostScript
Muhammad Torabi Dashti
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam
Tel: +31 (0)20 592 9333
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|