Game-based verification of contract signing protocols with minimal messages

Zhang, Ying, Zhang, Chenyi, Pang, Jun and Mauw, Sjouke (2012) Game-based verification of contract signing protocols with minimal messages. Innovations in Systems and Software Engineering, 8 2: 111-124. doi:10.1007/s11334-012-0180-9

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Zhang, Ying
Zhang, Chenyi
Pang, Jun
Mauw, Sjouke
Title Game-based verification of contract signing protocols with minimal messages
Journal name Innovations in Systems and Software Engineering   Check publisher's open access policy
ISSN 1614-5046
Publication date 2012-06
Sub-type Article (original research)
DOI 10.1007/s11334-012-0180-9
Volume 8
Issue 2
Start page 111
End page 124
Total pages 14
Place of publication London, United Kingdom
Publisher Springer
Collection year 2013
Language eng
Abstract A multi-party contract signing (MPCS) protocol is used for a group of signers to sign a digital contract over a network. We analyse the protocols of Mauw, Radomirović and Torabi Dashti (MRT), 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. 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 three 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 three and four signers, all of whom have been successfully model checked in Mocha.
Keyword Contract signing
Alternating-time temporal logic
Model checking
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2013 Collection
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: Scopus Citation Count Cited 3 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Thu, 11 Apr 2013, 15:23:51 EST by Ms Deborah Brian on behalf of School of Information Technol and Elec Engineering