Verification of MPCS protocols

• MPCS

Abstract

A multi-party contract signing (MPCS) protocol is used for a set of signers to sign a digital contract over a network. We follow the approach of Chadha, Kremer and Scedrov [CKS06] to analyse the protocols of Mukhamedov and Ryan (MR) [MR08], and of Mauw, Radomirovic and Torabi Dashti (MRT) [MRT09], using the finite-state model checker Mocha. Mocha allows for the specification of properties in alternating-time temporal logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives us an intuitive interpretation of the verification problem of crucial properties of MPCS protocols.
We analyse the MR protocol with up to 5 signers and our analysis does not reveal any flaws. MRT protocols can be generated from minimal message sequences, depending on the number of signers. We discover an attack on fairness in a published MRT protocol with 3 signers and a general attack on abuse-freeness for all MRT protocols. For both attacks, we present solutions. The abuse-freeness attack leads us to a revision of the methodology to construct an MRT protocol. Following this revised methodology, we design a number of MRT protocols using minimal message sequences for 3 and 4 signers, all of which have been successfully model checked in Mocha.

Note that for MRT protocols the attack on fairness was published in our FAST'09 paper [ZZPM09], and details on the abuse-freeness attack can be found in our technical report [ZZPM], which is under submission for publication. In order to use the following codes, first you need to install cMOCHA.

Model checking the MR protocol

We model the MR protocol with up to 5 signers and verify both fairness and timeliness properties, while Mukhamedov and Ryan only analysed fairness of their protocol with 5 signers. We write a C++ program mr-generating.cpp to generate models of the MR protocol with any number of signers. The program has been compiled using g++

g++ -o mr-gen mr-generating.cpp
./mr-gen number-of-participants out-file.

For instance, ./mr-gen 2 mr2.rm, ./mr-gen 3 mr3.rm and ./mr-gen 4 mr4.rm generate models with 2 signers as in file mr2.rm, with 3 signers as in file mr3.rm, and with 4 signers as in file mr4.rm respectively.

We can also generate a model for the MR protocol with 5 signers as in file mr5.rm. However, this model is too big to verify in Mocha. So we split the model into 16 sub-models which cover all the possible abort-chaining attack scenarios. Each of them focuses on one certain possible abort-chaining attack. We use iAjH.rm to indicate the model in which Pi aborts and collude with others to cheat Pj's signature. More discussion can be found in our paper [ZZPM]. These sub-models are given as follows:

1A2H.rm	1A3H.rm	1A4H.rm	1A5H.rm
2A1H.rm	2A3H.rm	2A4H.rm	2A5H.rm
3A1H.rm	3A2H.rm	3A4H.rm	3A5H.rm
4A1H.rm	4A2H.rm	4A3H.rm	4A5H.rm

Model checking MRT protocols

Using the notion of abort-chaining attacks, Mauw, Radomirovic and Torabi Dashti analysed the theoretical message complexity of MPCS protocols [MRT09]. Their results made it feasible to construct MPCS protocols excluding abort-chaining attacks but with minimal messages, which we call the MRT protocols, based on so-called signing sequences.

We describe how to construct an MRT protocol from a minimal signing sequence in our paper [ZZPM]. According to this method, we design a number of MRT protocols for 3 and 4 signers, all of which have been model checked in Mocha.
The following are the descriptions of MRT protocols built from different minimal sequences and their corresponding model in Mocha:

MRT protocols and models for minimal sequences with 3 signers

Sequence	Protocol description	Mocha model
s1: 12 | 3123 | 1232	mrt3-s1-protocol	mrt3-s1-model
s1: 12 | 3123 | 1232	mrt3-s1-fixed-protocol	mrt3-s1-fixed-model
s2: 12 | 3121 | 3212	mrt3-s2-protocol	mrt3-s2-model
s3: 12 | 3123 | 1321	mrt3-s3-protocol	mrt3-s3-model
s4: 12 | 31323 | 1321	mrt3-s4-protocol	mrt3-s4-model
s5: 12 | 31321 | 3123	mrt3-s5-protocol	mrt3-s5-model
s6: 12 | 3123 | 2132	mrt3-s6-protocol	mrt3-s6-model
s7: 12 | 3121 | 3123	mrt3-s7-protocol	mrt3-s7-model

For 4 signers, we can get 9 sequences distinct modulo isomorphism, we only choose 3 typical sequences, namely s2, s4 and s7, and design protocols for them:

• s1: 42314234 1243
• s2: 42314234 1234
• s3: 42314234 1324
• s4: 42314324 1234
• s5: 42314324 1342
• s6: 42314324 1324
• s7: 42312432 1423
• s8: 42312432 1432
• s9: 42312432 1342

MRT protocols and models for minimal sequences with 4 signers

Sequence	Protocol description	Mocha model
s2: 123 | 42314234 | 123432	mrt4-s2-protocol	mrt4-s2-model
s4: 123 | 42314324 | 123432	mrt4-s4-protocol	mrt4-s4-model
s7: 123 | 42312432 | 142324	mrt4-s7-protocol	mrt4-s7-model

mrt3-s1 is the example protocol described in [MRT09], and mrt3-s1-fixed is its fix.

Specifications in ATL

All contract signing protocols are expected to satisfy three security properties, viz. fairness, abuse-freeness and timeliness.

• Fairness. At the end of the protocol, either each honest signer gets all the others' signatures, or no signer gets any signature. Fairness ensures that no signer can get any valuable information without sending out his signature, and once a signer sends out his signature, he will eventually get all the others' signatures. An abort chaining [MR08] is a sequence of abort and resolve messages to the trusted third party T in a particular order, such that it enforces T to return an abort reply to an honest user who has already sent out his signature. The abort-chaining attack is a major challenge to fairness, and the resolve-impossibility result for a trusted third party has been proved for a certain class of MPCS protocols [MR08].
• Abuse-freeness. At any stage of the protocol, any set of signers are unable to prove to an outside observer that they have the power to choose between aborting the protocol and getting the signature from another signer who is honest and optimistically participating in the protocol. Intuitively, a protocol not being abuse-free implies that some of the signers have an unexpected advantage over other signers, and therefore they may enforce others to compromise on a contract.
• Timeliness. Each signer has a solution to prevent endless waiting at any time. That means no signer is able to force anyone else to wait forever.

Chadha, Kremer and Scedrov gave these properties in the alternating-time temporal logic (ATL) [CKS06]. fairness-n.spec, invfairness-n.spec and timeliness-n.spec give the specifications of fairness together with their invariant formulations, timeliness for each signer in the MR and MRT protocols with n signer.

fairness-3.spec	fairness-4.spec	fairness-5.spec
invfairness-3.spec	invfairness-4.spec	invfairness-5.spec
timeliness-3.spec	timeliness-4.spec	timeliness-5.spec

fairness-5-mr-special.spec is the specification for the MR protocol with 5 signers. commands.txt contains the verification commands in Mocha to verify fairness for a certain model.

Bibliography

[CKS06]	R. Chadha, S. Kremer and A. Scedrov. Formal analysis of multi-party contract signing. Journal of Automated Reasoning, 36(1-2), pp. 39-83, 2006.
[MR08]	A. Mukhamedov and M. D. Ryan. Fair multi-party contract signing using private contract signatures. Information and Computation, 206(2-4), pp. 272-290, 2008.
[MRT09]	S. Mauw, S. Radomirovic and M. Torabi Dashti. Minimal message complexity of asynchronous multi-party contract signing. Proc. 22nd IEEE Computer Security Foundations Symposium, IEEE Computer Society, pp. 13-25, 2009.
[ZZPM09]	Y. Zhang, C. Zhang, J. Pang and S. Mauw. Game-based verification of multi-party contract signing protocols. Proc. 6th Workshop on Formal Aspects in Security and Trust - FAST'09, Lecture Notes in Computer Science 5983, pp. 186-200. Springer-Verlag, 2009.
[ZZPM]	Y. Zhang, C. Zhang, J. Pang and S. Mauw. Game-based verification of contract signing protocols with minimal messages. Technical Report (submitted for publication), 2011