In [CKS04] we use the model-checker MOCHA to analyse two contract signing protocols. The first protocol was proposed by Garay and MacKenzie [GM99], the second by Baum-Waidner and Waidner [BW00].
We found several attacks compromising fairness in [GM99], as well as a curiosity when analysing abuse-freeness. When analyzing fairness in [BW00], we did not find any attack.
The verification with MOCHA [AHM+98] requires the specification of the system in reactive modules, as well as the specification of the properties using the ATL logic [AHK97]. We generate an instance (where the number of participants is given) by using a dedicated C++ program for each, the [GM99] and the [BW00] protocol.
Some slides are available here.
Download and instructionsBefore you are able to use the following programs you need to install cMOCHA (not MOCHA 2.0 !).
gm_protocol.cpp
is a C++ program which generates the reactive module description of
the [GM99] protocol
for a given number of participants.
The program has been compiled using g++ version 3.3.3.
Usage : ./a.out number_of_participants output_file
For instance,
./a.out 3 gm3.rm
writes the description of the protocol with 3 signers to the file
gm3.rm.
fairness-gm-3.spec
contains the specification of the fairness property for each of the 3
signers in the 3-signer protocol. The script fairness-gm-3.sl
contains the instructions for MOCHA. The
verification is launched by
mocha -t `pwd`/fairness-gm-3.sl
Note: You may have to edit fairness.sl to give a complete path of the
files gm3.rm and fairness-gm-3.spec.
Abuse-freeness is handled by the files abuse-freeness-gm-3-opt.spec, abuse-freeness-gm-3-opt.sl and gm3opt.rm. The file gm3opt.rm is a manually modified file, which models an optimistic participant P3, as proposed in [CMMS03]. We also show that the stronger version of abuse-freeness, proposed in [KR02], as well as an approximation of abuse-freeness do not hold, even in a non-optimistic setting. Therefore use files abuse-freeness-gm-3.spec and abuse-freeness-gm-3.sl on the previously generated gm3.rm file.
By running MOCHA in a similar way on the 4-signer version, we found the attacks compromising fairness. The used files are fairness-gm-4.spec and fairness-gm-4.sl.
Our corrected version of the protocol can be generated using gm_corrected_protocol.cpp. The verification uses the same fairness specification files as above.
The verification of the [BW00] protocol uses the following files.
Invariant checkingRecently, we have shown that when a contract signing protocol respects timeliness, verifying fairness can be realised using invariant checking. One of the major advantages of invariant checking is that in case the invariant is violated, a counter-example is generated. We first need to check that the protocol is timely (we verify two flavours of timeliness). This can be done for 3, respectively 4, signers using the following files.
The files used for the invariant checking of fairness are the following. To increase readability of the produced error-traces you can use the program clean.cpp which "cleans up" the trace. Here is an example of a cleaned error-trace. Bibliography| [AHK97] | Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In 38th Annual Symposium on Foundations of Computer Science, pages 100-109. IEEE Computer Society Press, 1997. |
| [AHM+98] | Rajeev Alur, Thomas A. Henzinger, Freddy Y.C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. MOCHA: modularity in model checking. In Alan J. Hu and Moshe Y. Vardi, editors, Tenth International Conference on Computer-aided Verification (CAV 1998), volume 1427 of Lecture Notes in Computer Science, pages 521-525, Vancouver, BC, Canada, June 1998. Springer-Verlag. |
| [BW00] | Birgit Baum-Waidner and Michael Waidner. Round-optimal and abuse free optimistic multi-party contract signing. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, Automata, Languages and Programming (ICALP 2000), volume 1853 of Lecture Notes in Computer Science, pages 524-535, Geneva, Switzerland, July 2000. Springer-Verlag. |
| [CKS04] | Rohit Chadha, Steve Kremer and Andre Scedrov. Analysis of multi-party contract signing. Technical Report no 516, Université Libre de Bruxelles. |
| [CMSS03] | R. Chadha, J. C. Mitchell, A. Scedrov, and V. Shmatikov. Contract signing, optimism, and advantage. In CONCUR 2003 - Concurrency Theory, volume 2761 of Lecture Notes in Computer Science. Springer-Verlag, 2003. |
| [GM99] | Juan A. Garay and Philip D. MacKenzie. Abuse-free multi-party contract signing. In Prasad Jayanti, editor, International Symposium on Distributed Computing, volume 1693 of Lecture Notes in Computer Science, pages 151-165, Bratislava, Slavak Republic, September 1999. Springer-Verlag. |
| [KR02] | S. Kremer and J.-F. Raskin. Game analysis of abuse-free contract signing. In 15th IEEE Computer Security Foundations Workshop, Cape Breton, Canada, June 2002. IEEE Computer Society Press. |