标题:Game-based verification of multi-party contract signing protocols
作者:Zhang, Ying ;Zhang, Chenyi ;Pang, Jun ;Mauw, Sjouke
通讯作者:Zhang, Y.
作者机构:[Zhang, Ying ;Zhang, Chenyi ;Pang, Jun ;Mauw, Sjouke ] University of Luxembourg, 6, rue Richard Coudenhove-Kalergi, L-1359 Luxembourg, Luxembourg;[Zha 更多
会议名称:6th International Workshop on Formal Aspects in Security and Trust, FAST 2009
会议日期:5 November 2009 through 6 November 2009
来源:Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
出版年:2010
卷:5983 LNCS
页码:186-200
DOI:10.1007/978-3-642-12459-4_14
摘要: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 Mukhamedov and Ryan (MR), and 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. 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 in a published MRT protocol with 3 signers, and present a solution for it. We also design a number of MRT protocols using minimal message sequences for 3 and 4 signers, all of which have been model checked in Mocha. © 2010 Springer-Verlag.
收录类别:EI;SCOPUS
Scopus被引频次:6
资源类型:会议论文;期刊论文
原文链接:https://www.scopus.com/inward/record.uri?eid=2-s2.0-77953256742&doi=10.1007%2f978-3-642-12459-4_14&partnerID=40&md5=413d54897af2705f605faca012773d00
TOP