Database of Case Studies Achieved Using CADP

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 our FTP 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: Dashti@cwi.nl



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


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


Back to the CADP case studies page