在电子商务迅速发展的今天,公平交易已成为安全在线交易的一个关键问题。多方合同签署协议MPCS (Multi-Party Contract Signing) Protocols是确保公平交易的重要协议。MPCS协议是多个参与者用来在网上签署数字合同的协议,它的安全性直接决定了电子商务交易的公平公正。因此,MPCS协议的构建以及其安全性的检测越来越成为研究的热点。最新的两个典型的MPCS协议是Mukhamedov和Ryan在2007年提出的MR协议和Mauw, Radomirovic和Torabi Dashti在2009年提出的MRT协议。本文利用有限状态模型检测机(Model-checker) Mocha,对这两个协议进行了安全性分析和验证。Mocha可以使用交替时态逻辑Alternating-time temporal logic (ATL)来描述属性,而ATL的博弈语义(game semantics)使ATL可以用竞赛树(winning strategies)的方式进行模型检测。这使得我们可以更为直观的理解MPCS协议关键属性的验证过程。本文的主要贡献有：第一,对MR协议进行model-checking验证,验证到5个参与者为止没有发现安全漏洞。第二,对MRT协议进行model-checking验证,检测出在09年发表的3个参与者的MRT协议存在fairness攻击,并给出了修正方案。第三,对Mauw, Radomirovic和Torabi Dashti的通过最短交换信息序列构造MRT协议的方法进行了完善并给出了形式化步骤。并根据完善后的步骤,为3个和4个参与者的所有做最小序列构建了相应的MRT协议。第四,通过对构建的MRT协议进行验证,发现了MRT协议存在关于abuse-freeness的攻击,并对该漏洞进行了修正。最后,对修正后的MRT协议进行Model-chekcing检测,结果显示,修正后的协议不存在fairness和abuse-freeness攻击。