Formal Verification of a Fair Payment Protocol.

Organisation:	CWI (THE NETHERLANDS)
Method:	mCRL (micro Common Representation Language) regular alternation-free mu-calculus
Tools used:	CADP (Construction and Analysis of Distributed Processes) (distributed) mCRL toolset
Domain:	E-commerce.
Period:	2004
Size:	12 properties
Description:	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 properties. 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.
Conclusions:	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.
Publications:	[Cederquist-Dashti-04] 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
Contact:	Muhammad 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 9333 Fax: +31 (0)20 592 4199 Email: [email protected]
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