第４ ４ 卷第１ 期２ ０ ２ １ 年１ 月计算机学报Ｃ Ｈ Ｉ Ｎ Ｅ Ｓ ＥＪ Ｏ ＵＲ Ｎ Ａ ＬＯ ＦＣ ＯＭ Ｐ ＵＴ ＥＲ ＳＶｏ ｌ ．４ ４Ｎｏ ．１Ｊ ａ ｎ． ２ ０ ２ １基于纳什均衡的智能合约缺陷检测陈晋川ｎ ’２）夏华辉”王璞巍＾马纳波ｕ王琪ｕ李浩然”杜小勇＆ｎＣ 中国人民大学信息学院北京１ ０ ０ ８ ７２ ）２）（ 数据工程与知识工程教育部重点实验室（ 中国人民大学） 北京１ ０ ０ ８ ７ ２ ）摘要本文研究区块链智能合约的缺陷检测问题， 即检测合约中是否存在部分合约方无论选择什么动作， 均无法避免损失的状态． 将智能合约问题转换成合约状态迁移图上的博弈策略选择问题， 提出了基于纳什均衡理论的合约缺陷自动检测方法， 以及为了提高检测效率， 提出了针对合约状态变迁图和博弈策略形式的一系列化简方法．最后， 实现了一个智能合约建模、分析和部署工具． 针对一组真实合同的实验表明， 该工具能自动发现部分合同缺陷， 化简方法提升缺陷检测效率的效果明显．关键词智能合约； 纳什均衡； 缺陷检测； 区块链； 博弈论中图法分类号Ｔ Ｐ３ １ １ＤＯＩ 号１ ０ ． １ １ ８ ９ ７ ／ ＳＰ ． Ｊ ． １ ０ １ ６ ．  ２ ０ ２ １ ． ０ ０ １ ４ ７Ｄｅ ｔ ｅ ｃ ｔ ｉ ｎｇＳｍａ ｒ ｔＣ ｏ ｎｔ ｒ ａｃ ｔＬ ｏｏ ｐｈ ｏｌ ｅ ｓＢ ａｓ ｅ ｄｏ ｎＮ ａ ｓｈＥ ｑｕ ｉｌ ｉ ｂｒ ｉ ｕｍＣ Ｈ Ｅ Ｎ Ｊ ｉ ｎ Ｃｈ ｕ ａｎ１ ） ， ２ ）ＸＩ ＡＨ ｕａ Ｈ ｕｉ１ ）ＷＡ Ｎ ＧＰ ｕ Ｗ ｅ ｉ１ ） ， ２ ５ＭＡ Ｎ ａ Ｂ ｏ１ ｝ＷＡ Ｎ ＧＱ ｉ１ ）Ｌ ＩＨ ａｏ Ｒａ ｎ１５Ｄ ＵＸ ｉ ａ ｏ Ｙ ｏ ｎ ｇ１） ，２）１ ：）｛ Ｓｃ ｈ ｏ ｏ ｌ ｏ ｆ Ｉｎ ｆｏ ｒｍａ ｔ ｉ ｏｎ  ？ Ｒ ｅ ｎｍｉ ｎ Ｕｎ ｉ ｖ ｅ ｒ ｓ ｉ ｔ ｙｏｆ Ｃｈ ｉｎ ａ ？ Ｂｅ ｉｊｉ ｎ ｇ１ ０ ０ ８ ７２ ）２ ） （ Ｋｅ ｙ Ｌａ ｂ ｏ ｆＤａ ｔａ Ｅｎ ｇｉ ｎ ｅ ｅ ｒ ｉｎ ｇａ ｎ ｄ Ｋｎ ｏ ｗｌ ｅ ｄｇ ｅ Ｅｎ ｇ ｉｎ ｅ ｅ ｒｉ ｎ ｇ ？ Ｍｉｎ ｉ ｓ ｔ ｒｙ ｏｆＥ ｄｕ ｃａ ｔ ｉ ｏｎ  ？ Ｒ ｅ ｎｍ ｉｎ Ｕｎ ｉｖ ｅ ｒ ｓ ｉ ｔｙｏｆ Ｃｈ ｉｎ ａ ？Ｂ ｅ ｉｊｉｎ ｇ１ ０ ０ ８ ７ ２ ）Ａｂｓ ｔ ｒａ ｃｔＩ ｎｒ ｅ ｃ ｅｎ ｔｙｅ ａｒ ｓ ， ｂ ｌ ｏ ｃｋ ｃｈ ａ ｉ ｎｈ ａｓ ａ ｔ ｔｒ ａ ｃ ｔ ｅ ｄｍ ａｎ ｙｉ ｎｔ ｅ ｒ ｅ ｓ ｔ ｓ ｆｏ ｒ ｍ ｂｏ ｔ ｈａ ｃ ａｄ ｅｍ ｉ ｃａｎ ｄｒ ｅ ｓ ｅ ａ ｒ ｃｈｃｏｍｍ ｕｎｉ ｔ ｉｅ ｓ ，ａｎ ｄ ｂｅ ｅｎａ ｐ ｐ ｌｉ ｅｄ ｉｎ ｃ ｒ ｙｐ ｔ ｏ ｃｕｒ ｒ ｅｎｃ ｙ ，ｆ ｉｎ ａ ｎｃ ｉ ａ ｌ ｔｅ ｃｈ ｎｉｑ ｕｅ ｓ ， ｌ ｏ ｇ ｉｓ ｔｉ ｃ ｓ ，ｃｏ ｐ ｙｒ ｉ ｇｈｔｐ ｒ ｏ ｔ ｅ ｃ ｔ ｉｏ ｎ ｅ ｔ ｃ ．Ｂ ｌ ｏ ｃ ｋ ｃｈ ａｉ ｎｉ ｓ ｂ ａ ｓ ｉ ｃ ａ ｌ ｌ ｙａｄ ｉ ｓ ｔ ｒ ｉ ｂ ｕｔ ｅ ｄｓ ｔ ｏ ｒ ａ ｇ ｅ  ｓ ｙ ｓ ｔ ｅｍ ，ｃ ｏ ｎ ｓ ｉ ｓ ｔ ｉ ｎ ｇｏ ｆ  ａ ｓ ｅ ｔｏ ｆ ｓ ｅ ｒ ｖ ｅ ｒ ｓｏ ｒ ｎ ｏ ｄ ｅ ｓ ．Ｉ ｎｂ ｌ ｏ ｃ ｋ ｃｈ ａｉ ｎｓ ｙｓ ｔ ｅ ｍｓ ，ｓ ｍａｒ ｔｃｏ ｎｔ ｒ ａ ｃ ｔ ｓ ａｒ ｅｗ ｉ ｄ ｅ ｌ ｙａ ｄｏ ｐ ｔ ｅｄ ａ ｓｔ ｈ ｅｃ ｏ ｄ ｅｌ ａ ｗ ｓ ｔｏ ｂ ｅｏ ｂ ｅ ｙｅ ｄｂｙａ ｌ ｌｐ ａ ｒ ｔ ｉ ｃ ｉ ｐ ａ ｎｔ ｓ ．Ｂ ｅ ｆｏ ｒ ｅ  ｓ ｔ ｏ ｒ ｉ ｎ ｇｔ ｈ ｅ ｄ ａｔ ａ ｉ ｔ ｅｍ ｉｎ ｔ ｏ ｂ ｌ ｏ ｃ ｋｃ ｈａ ｉ ｎ ， ｅ ａｃ ｈｎｏ ｄｅ  ｎｅ ｅ ｄｓ ｔ ｏ ｖ ｅ ｒ ｉ ｆｙｔ ｈ ｅｖ ａ ｌｉ ｄｉ ｔ ｙ ｏ ｆｔｈ ｉ ｓ ｏ ｐ ｅ ｒ ａｔ ｉ ｏ ｎ ｂ ｙｅ ｘ ｅ ｃ ｕｔ ｉ ｎｇ ｉ ｔ ｓｃｏ ｒ ｒ ｅ ｓ ｐ ｏ ｎ ｄｉ ｎ ｇｓ ｍａ ｒ ｔｃ ｏ ｎ ｔｒ ａ ｃ ｔ ｓ ，ｉ ． ｅ ．ｃｏｍ ｐ ｕ ｔ ｅ ｒｐ ｒ ｏ ｇ ｒ ａ ｍ ｓ ． Ｎ ｏ ｔ ｅ ｄ ｔｈ ａ ｔ，ｉ ｎ ｔｈ ｉ ｓ ｐ ａ ｐ ｅ ｒ ｗ ｅ ｆ ｏ ｃ ｕｓ ｏ ｎｃ ｌ ａｓ ｓ ｉ ｃ  ｓｍａ ｒ ｔ ｃｏ ｎ ｔｒ ａｃ ｔ ｓ ，ｉ ． ｅ ．ｃｏｍ ｐ ｕ ｔ ｅ ｒ  ｃｏ ｄｅ ｓ ｆ ｏ ｒｖ ｅ ｒ ｉ ｆ ｙｉ ｎｇ ， ｅｘ ｅ ｃｕｔ ｉ ｎ ｇ ， ｏ ｒ ｄｉ ｓ ｓ ｅ ｍｉ ｎａ ｔ ｉ ｎｇ  ｃｏ ｎ ｔｒ ａ ｃ ｔ ｓ ｉ ｎａ ｎｉ ｎ ｆｏ ｒｍａ ｔ ｉ ｏ ｎａ ｌｍａ ｎ ｎ ｅ ｒ ． Ｓ ｍ ａｒ ｔ ｃ ｏ ｎｔ ｒ ａ ｃ ｔｈ ａ ｓｂ ｅ ｃ ｏｍ ｅｏ ｎｅ  ｏ ｆ ｔｈ ｅ  ｃｏ ｒ ｅｔ ｅ ｃｈ ｎ ｉ ｑｕ ｅ ｓ ｏ ｆ ｂ ｌ ｏ ｃ ｋ ｃｈ ａ ｉｎ ， ａ ｎｄ ｉ ｔｉ ｓ ｖ ｅ ｒ ｙｉｍ ｐ ｏ ｒ ｔ ａｎ ｔｔ ｏ ｓ ｔ ｕ ｄｙｈ ｏｗ ｔ ｏｄ ｅ ｔ ｅ ｃ ｔｌ ｏ ｏ ｐｈ ｏ ｌ ｅ ｓ ｅ ｘｉ ｓ ｔｉ ｎｇ ｉ ｎｓｍａ ｒ ｔｃｏ ｎｔｒ ａ ｃ ｔ ｓ ． Ｈ ｅ ｒ ｅ ，ｔ ｈ ｅ  ｔｅ ｒｍｌ ｏ ｏ ｐｈ ｏ ｌ ｅ ｄｏ ｅ ｓ ｎ ｏ ｔｍ ｅ ａ ｎｂ ｕｇ ｓ ｉ ｎｔ ｈ ｅ ｃｏ ｎｔ ｒ ａ ｃ ｔｃｏ ｄｅ ｓ ， ｂ ｕｔ ｓ ｏｍ ｅ ｂａ ｄｏ ｕ ｔ ｐ ｕｔ ｓ ｏ ｆｅ ｘ ｅ ｃ ｕ ｔｉ ｎ ｇ ｔ ｈ ｅｃｏ ｎｔ ｒ ａ ｃ ｔｓ ．Ｔｈ ｅ ｓ ｅ ｏ ｕ ｔ ｐ ｕ ｔｓ ａｒ ｅｕ ｎｆ ａ ｖ ｏ ｒ ａｂ ｌ ｅ ｔｏ  ｓ ｏｍ ｅｃｏ ｎｔ ｒ ａ ｃ ｔ ｐ ａ ｒ ｔ ｎ ｅ ｒ ｓ ． Ｉｆ ａ ｌ ｌｐ ａｒ ｔ ｎ ｅ ｒ ｓ ａｒ ｅ ｒ ａ ｔｉ ｏ ｎａ ｌ ａｎ ｄｈ ａｖ ｅ ｃｏｍ ｐ ｌ ｅ ｔ ｅ  ｉ ｎｆ ｏ ｒｍａ ｔ ｉ ｏ ｎａ ｂ ｏ ｕ ｔｔｈ ｅ ｃ ｏ ｎ ｔｒ ａｃ ｔ ｓ ，ｔ ｈ ｅ ｓ ｅ ｏ ｕ ｔｐ ｕｔ ｓ ｃ ａ ｎｎ ｏ ｔｂ ｅ ａ ｖ ｏ ｉ ｄ ｅｄｎ ｏｍ ａ ｔｔ ｅ ｒｗ ｈ ａ ｔｃｈ ｏ ｉ ｃ ｅ ｓ ｔ ｈ ｅｐ ａ ｒ ｔ ｎ ｅ ｒ ｓ ｃ ｈｏ ｏ ｓ ｅｄ ｕｒ ｉｎ ｇ ｅ ｘｅ ｃｕ ｔ ｉ ｎｇ ｔ ｈ ｅｃｏ ｎｔ ｒ ａ ｃ ｔ ｓ ．Ｔ ｈ ｅ ｒ ｅ ｆ ｏ ｒ ｅ ｔ ｈ ｅ ｓ ｅ ｃ ｏ ｎｔ ｒ ａ ｃ ｔｓ ｗ ｉ ｌ ｌ ｎ ｏ ｔ ｂｅ ｃｏｍ ｅ ｒ ｅｐ ｅ ａ ｔ ｅ ｄｇ ａ ｍｅ ｓ ｓ ｉｎ ｃ ｅｓ ｏ ｍｅ ｐ ａ ｒ ｔ ｎ ｅ ｒ ｓ ｃ ａ ｎ ｎｏ ｔｂ ｅｎ ｅ ｆ ｉ ｔｆｒ ｏｍｊ ｏ ｉ ｎｉ ｎ ｇ ｔ ｈｅ ｃｏ ｎ ｔ ｒ ａ ｃ ｔ ｓ ．Ｔ ｈ ｅ ｓ ｅｋｉ ｎ ｄｏ ｆｃ ｏ ｎ ｔｒ ａｃ ｔ ｓ ｗ ｉｌ ｌｂ ｅｏ ｎ ｅ ｓ ｈｏ ｔｇ ａ ｍ ｅ ｓ ａ ｎ ｄ ａｒ ｅｈ ａｒ ｍｆ ｕｌｔ ｏ ｂ ｕｓ ｉ ｎ ｅ ｓ ｓ ｚｏ ｏ ｌｏ ｇ ｙ ．Ｗｅｐ ｒ ｏ ｐ ｏ ｓ ｅａｍｅ ｔｈ ｏ ｄｔ ｏｄ ｅ ｔ ｅ ｃ ｔ ｔ ｈ ｅｌ ｏ ｏ ｐｈｏ ｌ ｅ ｓｏ ｆ ｆ ｏ ｒｍａ ｌ ｉ ｚ ｅｄｓｍａ ｒ ｔ收稿日期： ２ ０ １ ９ １ ２ ０ ２； 在线发布日期： ２ ０ ２ ０ ０ ５ ２ ３ ． 本课题得到国家自然科学基金（ Ｕ １ ９ １ １ ２ ０ ３ ） 、贵州财经大学与商务部国际贸易经济合作研究院联合基金（ ２ ０ １ ７ ＳＷ Ｂ Ｚ Ｄ０ ８ ） 资助． 陈晋川， 博士， 副教授， 主要研究方向为分布式数据管理和区块链．Ｅ ｍａｉｌ ：ｅｄ ｕ． ｃ ｎ．夏华辉， 硕士研究生， 主要研究方向为区块链和智能合约． 王璞巍（ 通信作者） ， 博士， 副教授， 主要研究方向为服务计算和区块链．Ｅ ｍａ ｉｌ ：ｗ ａｎｇ ｐｕ ｗｅ ｉ＠ ｒ ｕ ｃ ．ｅ ｄ ｕ ． ｃ ｎ ． 马纳波， 硕士研究生， 主要研究方向为分布式计算和区块链． 王琪， 硕士研究生， 主要研究方向为区块链．李浩然， 硕士研究生， 主要研究方向为服务计算和区块链． 杜小勇， 博士， 教授， 主要研究领域为数据管理技术、语义网技术、智能信息检索技术．１ ４ ８ 计算机学报 ２ ０ ２ １年Ｎ ａｋ ａ ｍｏ ｔ ｏ Ｓ．Ｂ ｉ ｔｃ ｏ ｉ ｎ： Ａｐｅｅｒ ｔｏ ｐｅｅ ｒ ｅｌｅ ｃ ｔｒ ｏ ｎ ｉ ｃ ｃ ａ ｓ ｈ ｓ ｙ ｓ ｔｅｍ．２ ０ ０ ８． ｈ ｔ ｔｐ ｓ ： ／ ／ ｂｉ ｔｃ ｏｉ ｎ． ｏ ｒｇ ／ ｂ ｉ ｔ ｃｏ ｉ ｎ．  ｐｄ ｆＥ ｔｈ ｅｒ ｅ ｕ ｍ． ｈ ｔ ｔ ｐ ｓ ： ／ ／ ｗ ｗｗ ． ｅ ｔ ｈ ｅｒ ｅ ｕ ｍ． ｏ ｒｇＩ ｌ ｙｐ ｅｒｌｅｄ ｇｅｒ Ｆａ ｂｒ ｉ ｃ ， ｈ ｔ ｔｐ ｓ ： ／ ／ ｈ ｙｐ ｅｒｌｅｄ ｇｅｒ ｆａｂ ｒ ｉ ｃ ． ｒ ｅａｄ ｔ ｈｅｄ ｏ ｃ ｓ ．  ｉ ｏＫ ａ ｎ ｔ ａ ｒ ａＩｎ ｉ ｔ ｉａ ｔ ｉ ｖ ｅ， ｈ ｔ ｔ ｐ ｓ ： ／ ／ ｋ ａ ｎ ｔ ａ ｒ ａｉ ｎ ｉ ｔｉ ａ ｔ ｉ ｖ ｅ． ｏ ｒｇ技术也有了迅速发展．随着研究者对智能合约理解角度的不同， 智能合约的内涵逐渐泛化，一些研究者开始把智能合约广义地理解成“ 运行在区块链系统之上的一段计算机代码， 由共识机制确保代码的正确执行［２］ ”． 在本文中， 我们关注的是Ｓ ｚ ａ ｂ ｏ 所定义的经典智能合约：“ 以信息化方式验证、执行或传播合同的计算机代码随着区块链技术的发展， 智能合约变得越来越重要，现有的区块链系统都使用智能合约描述参与各方需要共同遵守的规则（ 合同条款） ． 例如， 在医疗数据共享领域， 通过智能合约来规范数据的产生者（ 病人） 、数据的保管者（ 医院） 以及数据的使用者（ 数据分析公司） 三方的权责利； Ｋ ａ ｎ ｔ ａｒ ａＩ ｎ ｉ ｔｉ ａ ｔ ｉ ｖ ｅ④ 则试图将区块链和智能合约变成一种法律条款的数字撰写平台；２ ０ １ ６ 年工信部发布的《中国区块链技术和运用１ 引§智能合约（ Ｓｍ ａｒ ｔ Ｃ ｏ ｎ ｔ ｒ ａ ｃ ｔ ） 的概念最早可以追溯到１ ９ ９ ４ 年， Ｓ ｚ ａｂ ｏ 将智能合约定义为“一种可以实现合同条款的计算机程序［ １ ］但是，一直到２ ０ ０ ８ 年区块链（ Ｂ ｌ ｏ ｃｋ ｃ ｈａ ｉ ｎ ） 技术出现之前， 智能合约都没能得到广泛关注． 原因可能是很难找到一种合适的技术可以在非完全信任环境中保证计算机程序正确执行和不会被篡改． 区块链源自于“ 比特币？ ”的底层技术， 是一种去中心化、不可篡改、多方共同维护的分布式计算和存储系统． 区块链网络中每个节点都是独立维护的， 通过一种分布式共识机制， 在没有权威中心节点的情况下， 确保各个节点数据保持完全一致． 研究者认为区块链系统非常适合为智能合约提供运行平台． ２ ０ １ ３ 年后出现的以太坊？ 和Ｈ ｙ ｐ ｅ ｒ ｌ ｅ ｄｇ ｅ ｒ Ｆａ ｂｒ ｉ ｃ？ 都提供了图灵完备的编程语言用于编写智能合约， 可以支持各种复杂的业务逻辑． 至此， 智能合约开始得到了越来越多的应用， 其ｃｏ ｎｔ ｒ ａ ｃ ｔ ｓ ｂ ａ ｓ ｅ ｄｏ ｎｔ ｈ ｅＮ ａ ｓ ｈｅ ｑｕ ｉｌｉｂ ｒ ｉ ｕ ｍｔ ｈ ｅｏ ｒ ｙ． Ｉ ｎ ｓ ｔ ｅ ａｄ ｏ ｆ ｈｉ ｒ ｉ ｎ ｇｌ ａ ｗ ｙｅ ｒ ｓ ｔ ｏ ｃｈ ｅ ｃ ｋｔ ｈｅｃｏ ｎｔ ｒ ａ ｃ ｔｔ ｅ ｒｍ ｓ ｏ ｎ ｅ ｂｙ ｏ ｎ ｅ， ｗ ｅｃ ａ ｎ ｎ ｏｗ ａ ｕｔ ｏｍ ａｔ ｉ ｃ ａ ｌ ｌ ｙ ｆｉ ｎ ｄｏ ｕｔｔ ｈ ｅｌ ｏ ｏ ｐ ｈ ｏ ｌ ｅ ｓ ｏ ｆｃ ｏ ｎ ｔ ｒ ａ ｃ ｔ ｓ ．Ｗｅｐ ｒ ｏ ｐ ｏ ｓ ｅａｄａ ｔ ａｓ ｔｒ ｕｃ ｔ ｕｒ ｅ ， ｃ ａ ｌ ｌ ｅ ｄ ｓ ｔ ａｔ ｅ ｔ ｒ ａ ｎ ｓ ｉ ｔ ｉ ｏ ｎ ｇ ｒ ａ ｐｈ ， ｔ ｏｄ ｅ ｓ ｃ ｒ ｉ ｂ ｅ  ｔｈ ｅ ｏ ｕ ｔ ｐ ｕ ｔ ｓ ｆ ｏ ｒ ｅ ａ ｃｈ ｐ ａｒ ｔｎ ｅ ｒｏ ｆ ｃ ｈ ｏ ｏ ｓ ｉ ｎ ｇｄｉ ｆ ｆ ｅ ｒ ｅ ｎｔ ｓ ｔｒ ａｔ ｅ ｇ ｉ ｅ ｓ ｏ ｆ ｅ ｘｅ ｃｕ ｔ ｉ ｎｇ ａ ｃ ｏ ｎｔ ｒ ａ ｃ ｔ ．Ｂ ａ ｓ ｅｄｏ ｎｔ ｈ ｅ ｓ ｔａ ｔ ｅ ｔ ｒ ａ ｎｓ ｉ ｔｉ ｏ ｎ ｇ ｒ ａ ｐｈ ，ｗ ｅ  ｆ ｕｒ ｔ ｈ ｅ ｒ ｄ ｅ ｆ ｉ ｎ ｅｔ ｈ ｅｐ ｒ ｏ ｂｌ ｅ ｍｏ ｆｓ ｍａ ｒ ｔｃ ｏ ｎｔ ｒ ａ ｃ ｔｇ ａ ｍ ｅ， ａｎ ｄ ｄｅ ｆ ｉｎ ｅ ｔｈ ｅ  ｌｏ ｏ ｐ ｈｏ ｌｅ ｓ ａ ｓ ａ ｓ ｐ ｅ ｃｉ ａ ｌｋｉｎ ｄｏ ｆＮ ａ ｓ ｈｅ ｑｕｉ ｌ ｉｂ ｒ ｉｕｍｓ，ｗ ｈ ｅ ｒ ｅｓ ｏｍ ｅｐ ａｒ ｔ ｎ ｅ ｒ ｓ ｗ ｏ ｕｌ ｄ ｏ ｂ ｔ ａｉ ｎ ｚ ｅ ｒ ｏｏ ｒ  ｎ ｅｇ ａｔ ｉ ｖ ｅ ｕ ｔｉｌｉ ｔ ｉ ｅ ｓ  ａ ｎｄ ｔｈ ｅｙ ｃ ａ ｎｎ ｏ ｔ ｉ ｍｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅ ｉ ｒ ｕ ｔ ｉｌｉ ｔｉ ｅ ｓｅ ｖ ｅ ｎｉｆ  ｔｈ ｅ ｙ ｃｈ ａｎ ｇ ｅ ｔ ｈ ｅ ｉ ｒ ｏｗ ｎ ｓ ｔ ｒ ａ ｔ ｅ ｇ ｉ ｅ ｓ ． Ｉ ｎｔ ｈ ｉ ｓｗ ａ ｙ ，ｗ ｅ ａ ｒ ｅａ ｂ ｌ ｅ ｔｏ ａ ｕｔ ｏｍ ａｔ ｉ ｃ ａ ｌ ｌ ｙ ｆｉ ｎ ｄｏ ｕｔ ｔ ｈ ｅｌ ｏ ｏ ｐ ｈ ｏ ｌ ｅ ｓ ｂ ｙ ｃｏｍ ｐ ｕｔ ｉ ｎｇ ｔ ｈ ｅＮ ａｓ ｈｅ ｑｕ ｉ ｌ ｉ ｂ ｒ ｉ ｕｍ ｓ ｏ ｆｓｍ ａｒ ｔｃｏ ｎｔ ｒ ａ ｃ ｔ ｇ ａ ｍ ｅ ． Ｈ ｏｗ ｅｖ ｅ ｒ ，ｔ ｈ ｅｓ ｔ ｒ ａ ｔ ｅ ｇ ｙｆｏ ｒｍ ｓｏ ｂ ｔ ａ ｉ ｎｅ ｄｆ ｒ ｏｍｔ ｈ ｅｓ ｔ ａｔ ｅ ｔ ｒ ａ ｎ ｓ ｉ ｔ ｉｏ ｎ ｇ ｒ ａ ｐｈｍａ ｙｂ ｅｔ ｏ ｏｌ ａ ｒ ｇ ｅｄｕ ｅｔ ｏ ｓ ｔ ａｔ ｅ ｅｘｐ ｌ ｏ ｓ ｉ ｏ ｎ ．Ｔ ｈ ｅ ｒ ｅｃｏ ｕ ｌｄｂ ｅｍｉｌ ｌｉ ｏ ｎ ｓｏ ｆ ａ ｎ ｄｅ ｖ ｅｎ ｌ ａ ｒ ｇ ｅ ｒ ｎｕ ｍｂ ｅ ｒ ｏ ｆ ｓ ｔ ａ ｔ ｅ ｓ ｉ ｎａ ｓ ｔｒ ａｔ ｅ ｇ ｙ ｆｏ ｒｍ ，ｗ ｈ ｉ ｃｈｃ ａ ｕｓ ｅ ｓ ｖ ｅ ｒ ｙｅ ｘｐ ｅｎ ｓ ｉ ｖ ｅ ｔ ｉｍ ｅ ｃｏ ｓ ｔ ｓ ｏ ｆ ｃｏ ｍｐ ｕｔ ｉ ｎ ｇＮ ａｓ ｈｅ ｑｕｉ ｌ ｉ ｂ ｒ ｉ ｕｍ ｓ ． Ｗｅ ｔ ｈ ｅ ｎ ｐ ｒ ｏ ｐ ｏ ｓ ｅ ｔ ｗ ｏ ｒ ｕ ｌ ｅ ｓ， ｉ ． ｅ ． Ｓｔ ｒ ａ ｔ ｅ ｇ ｙｅ ｑｕ ｉｖ ａ ｌ ｅｎ ｃ ｅ ａ ｎ ｄＮ ａ ｓ ｈｅ ｑｕ ｉｖ ａ ｌ ｅｎ ｃ ｅｒ ｕｌ ｅ ｓ ，ｆ ｏ ｒ ｓ ｉ ｍｐ ｌｉ ｆｙ ｉ ｎｇ ｔ ｈ ｅｓ ｔ ａ ｔ ｅ ｔｒ ａｎ ｓ ｉ ｔ ｉ ｏ ｎ ｇｒ ａ ｐｈａ ｎ ｄｓ ｔ ｒ ａ ｔ ｅ ｇ ｙｆｏ ｒｍ ｓ ， ｗ ｈ ｉ ｃｈ ｃ ａ ｎｇ ｒ ｅ ａ ｔ ｌ ｙｃｕ ｔｄｏｗ ｎ ｔ ｈ ｅ  ｔｉ ｍ ｅ ｃｏ ｓ ｔ ｓ ． Ｉ ｎｏ ｒ ｄｅ ｒｔ ｏ  ｆｕ ｒ ｔ ｈ ｅ ｒ ｃｕ ｔｄｏｗ ｎ ｔ ｈ ｅ  ｔ ｉｍ ｅ ｃｏ ｓ ｔ ｓｏ ｆｃｏ ｍｐ ｕｔ ｉ ｎｇ Ｎ ａ ｓ ｈｅ ｑｕ ｉ ｌ ｉ ｂｒ ｉ ｕ ｍ ，ｗ ｅａ ｌ ｓ ｏｐ ｒ ｏ ｐ ｏ ｓ ｅａｍ ｅ ｔ ｈ ｏ ｄｔ ｏｆｉ ｎ ｄｏ ｕｔｔ ｈｅｒ ｅ ｄｕ ｎｄ ａ ｎｔｓ ｔ ｒ ａ ｔ ｅ ｇ ｙｃｏ ｍｂ ｉｎ ａ ｔｉ ｏ ｎｓ ａ ｎｄｐ ｒ ｏ ｖ ｅｔ ｈ ａ ｔｗ ｅｃ ａ ｎｏ ｂ ｔ ａｉ ｎｔ ｈ ｅｓ ａ ｍ ｅＮ ａｓ ｈｅ ｑｕｉｌｉ ｂ ｒ ｉ ｕｍ ｓ ｗ ｈ ｅｎｔ ｈ ｅ ｓ ｅｓ ｔ ｒ ａ ｔ ｅ ｇ ｙｃｏ ｍｂ ｉｎ ａ ｔｉ ｏ ｎｓ ａ ｒ ｅｒ ｅ ｍｏ ｖ ｅｄ．Ｂ ａ ｓ ｅ ｄｏ ｎｔ ｈ ｅ ｓ ｅｍｅ ｔ ｈ ｏ ｄｓ ，ｗ ｅ ｄｅ ｓ ｉ ｇ ｎａ ｎ ｄｉｍ ｐ ｌ ｅｍ ｅｎ ｔａｔ ｏ ｏ ｌｆ ｏ ｒｍｏ ｄｅ ｌ ｌ ｉ ｎｇ ， ａ ｎ ａ ｌ ｙｚ ｉ ｎ ｇ ａｎ ｄｄ ｅｐ ｌ ｏ ｙｉ ｎ ｇｓ ｍａ ｒ ｔｃｏ ｎｔ ｒ ａ ｃ ｔ ｓ ．Ｗｅａ ｎａ ｌ ｙｚ ｅａｓ ｅ ｔｏ ｆ ｒ ｅ ａ ｌｃｏ ｎ ｔ ｒ ａ ｃ ｔ ｓ ｃ ｒ ａ ｗ ｌ ｅ ｄｆｒ ｏｍ ｔ ｗｏ ｐ ｒ ｏ ｆ ｅ ｓ ｓ ｉ ｏ ｎ ａ ｌｌ ａｗ ｙ ｅ ｒ ｗ ｅ ｂｓ ｉ ｔ ｅ ｓ ． Ｔ ｈ ｅ ｓ ｅ ｃｏ ｎ ｔ ｒ ａ ｃ ｔ ｓ ｃｏ ｖ ｅ ｒ  ｔｈ ｅ ｍａ ｉ ｎｃｏ ｎｔ ｒ ａ ｃ ｔ ｃ ａｔ ｅｇ ｏ ｒ ｉ ｅ ｓ ｌｉ ｓ ｔ ｅ ｄｉ ｎＣ ｏ ｎ ｔｒ ａ ｃ ｔＬ ａ ｗｏ ｆＰ ｅｏ ｐ ｌ ｅ？ｓ Ｒ ｅｐ ｕｂ ｌｉ ｃ ｏ ｆＣ ｈ ｉ ｎａ ． Ｗｅ ｄ ｉ ｓ ｃ ｕｓ ｓ ｓ ｏｍｅ ｃｏ ｎ ｔ ｒ ａ ｃ ｔ ｌ ｏ ｏ ｐｈｏ ｌ ｅ ｓ ｄｅ ｔ ｅ ｃ ｔ ｅｄｂ ｙｔ ｈ ｉｓ ｔ ｏ ｏ ｌ， ａｎ ｄｅｖ ａｌ ｕ ａ ｔ ｅｔ ｈ ｅａ ｂｉ ｌ ｉ ｔｙｏ ｆ ｏ ｕ ｒｐ ｒ ｏ ｐ ｏ ｓ ｅｄｍｅ ｔｈ ｏ ｄｓ ｔ ｏ ｉｍ ｐ ｒ ｏ ｖ ｅ ｔ ｈ ｅｐ ｅ ｒ ｆ ｏ ｒ ｍａ ｎｃ ｅ ．Ａ ｓｉｌ ｌ ｕ ｓ ｔ ｒ ａ ｔ ｅｄｂ ｙ ｔｈ ｅ  ｅ ｘｐ ｅ ｒ ｉ ｍ ｅｎ ｔ ａ ｌｒ ｅ ｓ ｕｌ ｔ ｓ ， ｏ ｕｒ ｍｅ ｔｈ ｏ ｄｓ  ｃ ａ ｎｇ ｒ ｅ ａ ｔ ｌ ｙｒ ｅｄ ｕｃ ｅ ｔ ｈ ｅ ｓ ｔｒ ａｔ ｅ ｇ ｙｆ ｏ ｒｍ ｓ ａ ｎ ｄｔ ｈ ｅｔ ｉｍ ｅ ｃ ｏ ｓ ｔ ｓ ．Ｋ ｅｙｗ ｏ ｒｄｓｓｍ ａ ｒ ｔｃ ｏ ｎ ｔｒ ａ ｃ ｔ；Ｎ ａ ｓ ｈ ｅｑ ｕｉｌｉ ｂｒ ｉ ｕｍ ； ｌ ｏ ｏ ｐｈ ｏ ｌ ｅ ｄｅ ｔ ｅ ｃ ｔｉ ｏ ｎ ； ｂ ｌ ｏ ｃｋ ｃｈ ａ ｉ ｎ ； ｇ ａｍ ｅ ｔ ｈｅ ｏ ｒ ｙ①②③④陈晋川等： 基于１ 期 纳什均衡 的智能合 约 缺陷检测 １ ４ ９发展白皮书》［ ３ ］， 将智能合约解释为一种用计算机语言取代法律语言去记录条款的合约． 我们期待智能合约可以逐渐替代部分传统合同． 但是， 智能合约并没有统一的编程语言和运行模型． 这就使得程序员之外的管理人员难以理解和编写智能合约． 例如， 以太坊使用Ｓ ｏ ｄｉ Ｕ ｔ ｙ 编写智能合约， 将其实现为一种状态机？； Ｈ ｙｐ ｅ ｒ ｌ ｅｄｇ ｅ ｒＦ ａ ｂｒ ｉ ｃ 智能合约被称为链码（ Ｃ ｈ ａｉ ｎ ｃｏ ｄｅ ） ， 使用Ｇｏ 语言编写， 没有全局状态， 对区块链的读写都需要经过链码来执行．接下来， 我们用一个非常简单的买卖合同例子分析智能合约编写面临的问题：“ 卖方发货， 买方将钱转账给卖方编写这样的智能合约， 我们首先遇到的问题是：如何构建一种与编程语言和平台无关的、易于理解的中间模型？ 文本合同是由参与各方的管理人员（ 律师） 用自然语言撰写的， 然而智能合约需要使用计算机编程语言实现， 因此又要由专业的程序员编写． 由于自然语言和程序语言之间的差别， 双方可能无法准确理解彼此的意图． 例如， 上述例子中没有明确说明“ 卖方什么时候发货”， 这给智能合约代码的编写带来困难， 他们之间缺少一种双方都能准确理解的中间模型（ 类似数据库领域的Ｅ Ｒ 模型） ， 这就是智能合约建模问题；此外， 我们还会面临第二个问题： 如何发现智能合约中存在的逻辑缺陷？ 智能合约是由计算机代码构成的， 现有的一些方法提出使用检测工具对智能合约代码进行检测以找出其中存在的漏洞［２］． 然而，智能合约的一些重要缺陷， 其实不是代码漏洞， 而是逻辑缺陷． 例如， 前面例子中的买卖合同存在着一个对卖方不利的执行路径：“ 卖方发货， 买方不转账我们需要对智能合约进行分析以判断是否存在这样的逻辑缺陷， 这就是智能合约的缺陷检测问题．对于第一个问题， 我们之前提出了一种智能合约形式化模型［４］． 首先， 站在管理人员的角度， 采用多Ａ ｇ ｅｎ ｔ 领域的承诺（ ｃｏｍ ｍｉ ｔ ｍｅ ｎｔ ） 模型［５］， 将智能合约看作是一组“ 承诺” 的集合． 承诺描述了参与各方要执行的动作； 其次， 站在程序员的角度， 将智能合约看作是一种基于承诺生成的状态机， 描述智能合约的执行过程． 在之前工作的基础上， 本文提出从承诺到状态机的自动生成算法． 但在这个生成过程中， 往往会遇到“ 状态爆炸”问题， 也就是会产生指数级的数量巨大的状态， 导致生成算法无法高效完成．为了应对这个问题， 本文又提出了一系列的化简算法， 可以极大地提高状态机的生成效率．对于第二个问题， 根据智能合约参与各方选择的动作不同， 智能合约将进人到不同的状态， 形成不同的执行路径． 我们提出把这种执行过程看作是一个多方博弈问题［６］： 各方将会从智能合约中获取或损失收益， 他们是理性的， 会以收益最大化为目的来选择如何执行动作． 智能合约中的逻辑缺陷实际上是指部分参与人会陷人到一种局面， 无论他们选择什么动作， 都无法避免收益损失． 我们提出用“ 纳什均衡（ Ｎ ａ ｓ ｈＥ ｑ ｕｉｌｉ ｂｒ ｉｕ ｍ ）” 思想来捕捉这样的缺陷．纳什均衡是博弈论中的重要理论， 对于参与博弈各方所能选择的策略， 存在这样的策略组合： 各参与方均不能通过单方面改变自己的策略来获取更好的收益． 例如， 考虑一个简单买卖合同， 卖方有两种可以选择的策略｛ 发货， 不发货｝ ， 买方也有两种策略｛ 转账， 不转账｝ ． 对于策略组合｛ 卖方不发货， 买方不转账）？， 卖方和买方单方面更改策略都会面临收益损失： 如果卖方将策略改为发货， 买方还是不转账， 这会使得卖方出现收益损失； 同样如果买方将策略改为转账， 卖方还是不发货， 也会使得买方收益损失．这样的策略组合就称为纳什均衡点， 它体现了博弈的均衡状态， 在此状态下各个参与人都倾向于采取理性的行动．我们定义合同的逻辑缺陷就是特殊的纳什均衡． 如果合同的纳什均衡点中， 各参与人的收益全部为零， 或者收益有正有负， 那么这个合同就可能有逻辑缺陷， 因为部分参与人无法取得正收益， 他们将不再倾向于参与合同． 上述简单买卖合同例子中， 唯一的纳什均衡点就是｛ 卖方不发货， 买方不转账｝ ， 此时双方收益均为零． 原因在于该合同中没有对买方违约行为（ 不转账） 进行约束． 那么理性的卖方在权衡得失之后， 将选择不执行合同． 这样的合同对双方都没有价值．对于简单的合同， 执行路径较少， 容易以人工的方式发现逻辑缺陷． 但是对于复杂的合同， 其执行路径将非常复杂． 即使受过专业训练的律师也可能难以发现合同中所有的逻辑缺陷． 当合同以智能合约的形式存在， 人工检测逻辑缺陷将更不可行．本文的贡献如下：（ １ ） 提出一种基于纳什均衡的智能合约缺陷分①Ｅ ｔｈ ｅｒ ｅ ｕ ｍ．ｈ ｔ ｔ ｐ ｓ ：  ／／ ｓ ｏ ｌｉ ｄ ｉ ｔｙ ， ｒ ｅａ ｄ ｔ ｈ ｅｄ ｏ ｃ ｓ ． ｉｏ ／ ｅ ｎ ／ ｖ Ｏ ． ４ ． ２ １ ／ｃ ｏ ｍ ｍｏ ｎ ｐ ａｔ ｔ ｅ ｒ ｎ ｓ ， ｈ ｔ ｍｌ Ｅ ｓ ｔ ａｔ ｅ ｍ ａｃ ｈ ｉ ｎ ｅ１ ５ ０ 计算机学报 ２ ０ ２ １年析方法． 形式化定义了智能合约的博弈问题、策略形式和纳什均衡； 将智能合约的缺陷检测问题转换成了纳什均衡计算问题， 通过对智能合约逻辑缺陷的分析， 可以将逻辑缺陷以及相应的收益情况反馈给用户， 避免因为智能合约的逻辑缺陷给用户带来损失；（ ２ ） 提出了一种基于智能合约形式化模型的纳什均衡检测算法． 将形式化定义的智能合约转换为状态变迁图； 基于策略等价原则和纳什均衡等价原则， 提出了一系列状态变迁图的化简方法， 极大地避免了状态爆炸； 然后根据简化的状态变迁图， 提出了冗余策略的化简方法， 进一步提高计算纳什均衡的效率；（ ３ ） 依据《中华人民共和国合同法》（ １ ９ ９ ９ 年３ 月１ ５ 日颁布） ， 常见的合同共有１ ５ 类． 我们参照华律网（ ６ ６ ｌ ａ ｗ ． ｃ ｎ） 和合同帮（ ｈ ｅ ｔ ｏｎ ｇ ｂ ． ｃｏ ｍ） 的合同范本，对其中１ ４ 类合同进行了分析， 找出了其中真实存在的合同缺陷， 说明方法的有效性； 并通过实验分析了所提出的化简方法的效率．本文第２ 节介绍智能合约建模和分析的相关工作； 第３ 节介绍如何为智能合约建模， 以及智能合约的状态机生成算法； 第４ 节介绍智能合约的博弈问题； 第５ 节介绍状态变迁图的化简方法， 以及冗余策略组合的化简方法； 第６ 节通过实验说明所提出方法的有效性和效率． 最后， 第７ 节进行总结和对未来工作的展望， 本文工作并非提出新的智能合约， 而是将合同建模为状态机， 并基于此建模方法对合同进行分析．２ 相关工作智能合约漏洞暴露出来的安全性事件一直层出不穷， 例如， ２ ０ １ ７ 年发生的ＤＡ Ｏ ① 事件， 黑客利用智能合约的漏洞将面向公众筹集的大量以太坊代币转向自己的地址， 造成了巨大的经济损失． 因此， 智能合约安全性一直受到研究者广泛关注， 目前很多工作采用软件工程领域的代码检测方法来做智能合约代码漏洞检测． ２ ０ １ ６ 年， Ｈ ｍ ｎ ？ 提出将智能合约代码转换为Ａ Ｖ Ｌ 树， 然后利用Ｉ ｓ ａ ｂ ｅ ｌ ｌ ｅ 定理证明器对Ａ Ｖ Ｌ 树进行验证， 找出智能合约的代码漏洞．Ｙ ａ ｎｇ 等人［ ７ ］ 提出一种符号模型（ Ｓ ｙｍｂ ｏ ｌｉ ｃ Ｐｒ ｏ ｃ ｅ ｓ ｓＶ ｉ ｒ ｔ ｕａ ｌＭａ ｃ ｈｉ ｎ ｅ ， ＦＳ ＰＶＭ ） 用于刻画智能合约的执行流程， 然后基于Ｈ ｏ ａｒ ｅ 逻辑验证智能合约代码的可靠性和安全性． Ｂ ｌ ｇ ｌ 等人［ ８ ］ 认为智能合约中参与人之间存在非合作博弈， 在假设他们是理性的前提下分析他们可能采取的策略， 在此基础上生成一种概率模型， 再检测智能合约的安全性． 上述这些工作目的是为了检测智能合约代码的安全漏洞． Ｂｌ ｇ ｌ 等人虽然提到了博弈论的概念， 但也只是为了分析合约参与人可能的行为， 并没有考虑合约公平性的问题．不同区块链系统有不同的智能合约运行模型．例如， 以太坊是公有链， 任意节点都可以加人参与交易． 它的智能合约用Ｓ ｏ ｄｉ Ｕｔ ｙ 编写， 以字节码形式存储于区块中， 可以被各个节点执行． 智能合约在发布之后可以被多次调用， 每次调用均需从之前的区块中读取合约的状态和字节码， 而执行的结果也会存人新的区块中． 因此， 智能合约在以太坊上的执行可以看作是一个状态机， 每次执行将会从一个状态转移到另一个状态［９］＿Ｈ ｙｐ ｅ ｒ ｌ ｅｄｇ ｅ ｒＦ ａ ｂｒ ｉ ｃ 是使用最广泛的许可链， 节点需要经过授权才能参与交易． 与以太坊不同的是， 它的智能合约（ 链码） 并不存储于区块， 而是一直运行在联盟节点的ｄｏ ｃ ｋ ｅ ｒ 容器之中． 采用Ｇｏ 语言编写， 对区块链数据的读写都要通过链码执行（ 但链码本身不记录执行后的状态） ． 需要注意的是， 智能合约是一个概念， 指一种可以实现合同条款的计算机程序， 本质上智能合约与区块链是独立的． 链码是Ｈ ｙｐ ｅ ｒ ｌ ｅ ｄｇ ｅ ｒＦ ａ ｂｒ ｉ ｃ 系统中实现智能合约的方式， 在发展过程中超越了传统智能合约的概念． 本文讨论的智能合约是一个状态机， 是程序化的合同条款， 我们将基于承诺模型来描述合同并自动生成相应的状态机．在多Ａｇ ｅｎ ｔ 领域中， 承诺（ ｃｏｍ ｍｉ ｔ ｍｅ ｎｔ ） 模型通常用来研究多个主体之间的交互协议． Ｓ ｍｇｈ 等Ａ［５ ａ °］ 形式化定义了承诺模型， 认为承诺是商业关系的基本抽象， 是商务合同的本质． 承诺是有状态的， 例如， 完成、违约和过期等． 对于每个承诺， 有操作（ 动作） 可以触发其状态发生变化． 不同承诺之间存在相互影响关系， 多个承诺就构成了多个主体之间的商业协议［ １ １ ］． 在承诺模型的基础上， Ｓｎ ｇｈ 等人［ １ ２ ￣］ 又提出了商业合同公平性和健壮性等属性的检测方法， 基本思路也是判断各方是否都从合同中收益或者合同执行是否会进人非法状态． 这些工作没有考虑商业合同运行在区块链之上的情况， 本文①Ｔ ｈ ｅＤ ＡＯ． ｈ ｔ ｔ ｐ ｓ ： ／ ／ ｇ ｉ ｔ ｈ ｕ ｂ ． ｃ ｏ ｍ／ ｓ ｌ ｏ ｃ ｋ ｉ ｔ ／ ＤＡ Ｏ②Ｉ ｌ ｉ ｒ ａ ｉＹ ．Ｆ ｏ ｒ ｍａｌ Ｖｅｒ ｉ ｆ ｉ ｃ ａ ｔ ｉ ｏ ｎ ｏ ｆ Ｄ ｅｅｄ Ｃｏ ｎ ｔ ｒ ａ ｃ ｔ ｉ ｎ Ｅ ｔｈ ｅｒ ｅ ｕ ｍＮ ａ ｍｅ Ｓｅ ｒ ｖ ｉ ｃ ｅ ，２ ０ １ ９ ．ｈ ｔ ｔ ｐ ｓ ： ／ ／ ｙ ｏ ｉ ｃ ｈ ｉ ｈ ｉ ｒ ａ ｉ ． ｃ ｏ ｍ／ ｄ ｅ ｅｄ ， ｐ ｄ ｆ離劑等Ｉ．霜１ 期 于靖计禅衡的臂俱脅约缺陷錄 １ ５ １提出在承诺模塑的基■础上构靡智能合约（ 商业合同） ５ 搏设计算怯从一组承诺＿ 动生成运行隹型（ 也就是狀态机模爾）？ 然后在状态机模：型的基础上．动分析智能含约， 检测出可能存在的？辑缺陷． 在文献［ １ １ ］ 中， 也提出采用纳什均衡来分析合同的芷确性（ ｉＳｔ ｉ池ｃｔ ｎ ｅｓ轉， 但其方機需醫＇齋華博虐：树中所有可＇能的路径． 役有做任何化简■■ 在敢率上与我们所实现的Ｍｓ＆ｌｉ ｎ ｅ 方法（雜８； ， 中的ＳＥ 方法３： 相综上所述现有的智能合釣分析工作主驀还是进行代码漏洞分析， 缺少对费约中逻辑缺陷的分析？此外， 现有区块链系统的智能合约运行樓型各有不同， 缺少一种统一的、无关于编程谱有和平舎的智能合约模型＊ 甩于支持这种分析． 本文提出了一种易于痤解的、编程语言无关的智能合约模型以及基于纳什均衡理论提出了一种脅约缺陷检铡方法．３ 智能合约的建模承诺模型在多Ａｇ ｅｎｔ 领域被广泛用宁对跨组。织协议的建模￥９ １ ２ ］． 本文提出智能合约建模首先＿用户将合同条款以“ 承诺”的形式描述， 然后再基于用户书写的承诺自动构建智能合约． 本节介．绍如何定ｉｃ＇ 承诺＇ 以及如何儀Ｔ一组承诺＿ 动构建智能合钓的状态机？３． １承诺定义１ ＿承谱ｆ ｅａｍｍ ｉｔｍ ｅｎ ｔ）？一个承谨是一个五兀组ＣＣ ａ ｓ ， ＿ｖ ，｜＜ ， ， 表市攀向＿ｖ 承诺， 見謹肅提条件Ｋ ｐｒ ｅｍｉ ｓ ｅ） 瘸足， 就＃在ｋ 规定的时间期限完：威Ｋ触ｔ ｉｌ ｔ ） ？定义２ ． 承诺的生命周期？一个承诺可能具有五种不同的状态＊ 其．生侖Ｍ 期可以用一个状态机表示， 如＿ １ 所示．ａｃｔ （ ｌ ） Ｃ（ｘ， ｙ，ｐ， ｒ ，ｔｃ ）ｔｉｍｅｏｕ ｔＣ （ｘ， ｙ，夕，ｒ，ｆａｌｓｅ ） ｅｘｐ （Ａ ）ｐ＝ｔｒｕｅ６ａｓ （ ２ ） Ｃ（ ｘ， ｙ ， ｔｒｕｅ，ｒ ， ￡ｃ）＾ｍｅｏｕ，－＞Ｃ （ ｘ＾ｙ，ｔｎ ｉｅ， ｒ， ｆａ ｌｓｅ ） ｖｉ ｏ （５ ）ｓａｔ（ ３ ） Ｃ （ａ：，３＞，ｔ ｒｕｅ，ｔｒｕｅ，ｉｃ ）图ｉ 最ｉｆ銳命屬＿如图ｌ 所示，一个承诺的生命周期内可能有五种不同的状态， 其中激活（ 《戊１ 是初始状态》终止状＿纛蠢彳过期（：＊＊ ＃） ｆｊｉ：约）， 病嚴：（ １ ． ） 撒活（似） ． 当前提户和结果ｆ 的值都未知，并且＾？ 处于有效期／本文用数宇１ 表示＿（ ２ ） 就：靖ｆ办狀ｈ 前攝户涂ｔ ｒｕ ｅ？零皋ｒ米麵， 并且的＾ 并未超出有效期？ 此时则表示前撻ｆ 已鐵达成， 等待结果的竞成。本文用数字２ 表示．＿ 橋足Ｃ ｓｆｉ ｄ． 当一个：攀舉截Ｔ雜＿之錄！＿责任言工１３成了绪：果＂■承诺迸人满： ■￡（：．？？ ） 状态，毫示承诺完成． 本文用数字３＿ 示．Ｕ） 过期（ ｅ：＃， ） ． 若承诺原本处于激活态＊ 但如果超出了时间约束， 师承诺进入过期状态． ． 表；示承谱已羟失数， 本Ｘ用数字４ 表示－违约（ ｔＡ） ． 承诺进入就绪态， 前提＞已絰满足， 但衰任方＇ ＊ 没有在规定的时间ｆｒ完成结渠ｒ ，．则承诺迸人违约状态． 本文用数字５ 表示．承诺的前提条件ｆ 長一个逻辑表达式， 组成表：达式的每个文字（ ｌ ｉ ｔｅｍ Ｄ可以是一个布尔条件， 表示某个承诺处于某个状鑫， 例姐若承诺Ｃ２ 的前提＞＝表示必须Ｇ 的状态为之后， ＆才可以就绪． 前提的文字也可以是一个布尔函数形式的仲裁结果， 表示由第三方判定某个条件是否成立． 例如，在某运输合同中有一个承诺， 春出现自然灾害， 则承运方无衝＾赔偿， 那么承诺的前提条件就应包括乂Ｋ 〇％ｅ （ 自然戴害Ｘ 本文使思ｊＷｇｅ 函数来表藏仲裁， 仲裁可以＿ 智能脅约瑱育机ｃｗ （ 监控Ｋ 块链事件并能将监控结某发回智能合约） 或合同双方共同指麵愈第三方蠢成＊ 蠻藝證出， 预言机■ 第三方只鬱赛对所规定的事项作出仲裁， 而不是仲裁整个合同的执行状况．ｒ 称为承诺的结果＊ 晕一组动作的合取式－时间雜索紀包＇含两个部分， 即纪：＝ 如加瑪《山分别表示当承诺进人，或＆？ 之后， 承诺应该在或扛－ 醜軸窟珙．例１．—个筒单翁购书合ｆ＇承谱在Ｓ 天内忖拿１ 〇〇元， ３獻爾審收到书擊之Ｂ Ｉ 天为鼕赁，Ｇ （ 伊， 乙， ０ ， ｜ｗ ｉｙ（ Ｚ ，１，？： ）＊ （ ＊３ ） ） ，Ｃ２ （ Ｚ ＞ ＾＾ ０％ ， ｓ ａｔ ＾ｄｅ ｌ ｉ ｉ ＜ｅｒ（，ｂｏｇ ｋ ＜ ＾ ） ． （ １ ． １ ） ） ．承请戌的含Ｘ 是甲向乙承诺》在３ 天内付款１ 〇〇元． 法意此承诺的前提： 条件为空． 即不设前提？并且此承诺在前提满足之后３ 天内必舊晃成动作ｐａｙ ｉ Ｚｊ  ． １ ０ ０ ５ ．承诺＾ 的含义是， 当承诺Ｃ： 进人如状态（ 即：甲在３ 天内付款则乙承诺在ｉ 天内发货？ 注意该承诺的时间约束的．第一部分为；｝ 天， 含义是在合约签署３ 天之后， 该承诺过期？ 也就是说即使甲在３ 天１ ５ ２ 计導机攀报 ：＿１苹之后窟成承诺ｃ＼ ， 乙也没有义务发货．３ ． ２ 智能合约定义３？智衝合釣Ｃｆｅｍ ｓｔｆｔ「初ｎ ｔｒ ａＭ） ．—个智能含约是一个确定性有穷状态机（ ＤＦＡ ） ， 即Ｓ Ｃ ：＝｛， ＣＣｆ Ｓ ｉ Ｓ ｆｓ〇， Ａ ， ｒ ）：（ １ ）ＣＣ ＝ ！ Ｃ！ ，？ ” 》．Ｃ；Ｕ 袭示一组承诺；（ ２） ５ 是字母表， 包括所有可触发ＣＣ 中一今或■个承诺谶慶状＿ 的導件．一个審件可Ｍ ；叢一个动作， 某个仲裁的绪果， 或是某个承诺状态发生改变（ 比如过期） ；＿Ｓ＝ ＇！ ％，＊＞、， 心Ｕ 暴有｜艮个状态的＇ 集合．ｓ，．Ｃｉ＝ 〇，…， ？ 》） 是一？个《维＿ 量， 即Ｓ； ３ 霉ｉ —痛ｉｆ，…，Ｃ？ ． ｓ ｉＵＭ＾＾（． ｓｔａｔ ｅＳ？ｉ〇． ｃｔ－： ． ｓＭｉｅｘｐ？ｔａ ｏ ｝ ）（ ４）  ５ ａ £ Ｓ 是初始状态， 若一个承诺的前提为壑， 贝丨１眞＿ 絳中状态为ｆｅｉｑ—施其截霧为ｄ ｒｆ；（ ５ ） ＺｂＳ其羞一＃ 綦状态较穆画数；ｊ一个状态转＾＇（Ｓｔ ＜， ： ｅ） ＞ －Ｓｊ￡： Ｚ ＼ ｉｆ ｆＣＤ＊ 和？ 两个ｆｅｆｔｇｆｅｇ Ｉ 雜Ｊｌ的取值不區ｔＡ＝１？ ？ ） ． Ｊ＝Ｌ？） ： 依据Ｇ 的定义， 当事件ｅ ６ ５ 发生， ＣＡ 的状态应从書为＊！ ■ ］（： ？是一钽接受：的状＿ ｃ：馨态）， ｖ ｓ， ｅ ， ，｛ｓ ａ ｌ ， ｅ＾ｘｐ． ＜＇ｖｉｏ ｝ （ ｋ＝ ｌ ．图￡中展示的是根据例１ 中的承诺得到的智能合约？ 如ａ２ 所示， 合約的初始状态（． 裉，结点） 为（ ２ ， １ Ｓ ， 国为承诺ｃ＼ 前提为痊， Ｍ 此其初始状态为２ Ｃ ＆ａｘ） ． 图Ｐｐ 斑上最出了遽变含约狀态的書件， 比如在初始状态可以象：■寶个事件， ｆ細ｅ〇？ｌｆｅｙ＜ Ｃｉ ：） 和前春Ｃｉ 在进人Ｗｓ 之后：超时， 也雜倉祿翁歲：承诺违翁， 因此转变勤狀态Ｃ ５，１ ）， 表示：■诺的拔态展２ （＆？ｓ ） 改变愈ｇ ｔｆｅｉ ｏ：） ．． 爵一个＿件， 參示甲执行付款动作， 使得承诺＆ 从２ （ ＆？ ） 改变为为进人到〇的前槔得到满足， ：真状态售动从１ Ｃ财ｉ ：》变为２ （知功《菌此我们導到状處ｔ３？ ２ ） ？ 洼參， 当一个擧诺：的翁禪变为ｔｒ ｕｅ？ ＿状高將ｅ＾ｔ ｉｍｅｏｕｔｊｊａｓ（Ｑ ）（ ５〒１ ）乙 Ｃ（ ３，２ ）ｅ３＝ｔ ｉｍｅｏｕｔ－ ａｃ ｔ （ｐ２）ｒ？４＝ ｄｅｌ ｉｖｅｐ／，＇Ｃ ５ ？４ ）Ｅ（ ３，３ ）乙＝ｔｉ ｍｅｏｕｔ＿ ｂａ ｓ（Ｃ２  ）（ 〇，〇） （ １０，１０ ）Ｆ（ ３，５ ）（－１０ ０，１０ ０ ）图２ＤＦ八形式的智能合约自动从１ 变：更为２ ＊无醫颡外事＃ 触发？ 寅此本文描述中都略去了从１ 到２ 的状态变化过程．３ ． ３ 由承诺生成状态机根据一组承诺， 我们可以有动构造相应的ＤＦＡ．算法如卞．算法１ ． 创建Ｄ ＦＡ ．翁入ｔ 一组承雷￡£：输ＳｈＫＦＡ 的根鷄＾１．ｎ Ｑ—ｉ ｎｉ ｔＲ ｏ ｏ Ｋ ＣＣ） ； ／ ／ｗＱ 是ＤＦ八根结点２． Ｈ． ｆ ＭｓＭ ｎ。）； ／ ／ ／／ 是一个堆栈， 存放状态结点３ ．Ｗ Ｈ ＩＬＥ Ｃ Ｈｎ ｏｔ ｅｍｐ ｔｙ）Ｄ Ｏ ｛４．ｎ ＾Ｈ． ｐｏｐ ｉ ）；５．ｓ —ｎ． ｓｔ ａ ｔ ｅ；６．ＦＯＲ （ ｅ ａ ｃ ｈＺ 满足（ ５ ， ｅ ）—５＇£ ｄ ）Ｄ Ｏ ｛７．ＩＦ  （／ £ Ｈ）Ｔ ＨＥＮ ｆ／ ／若该状态曾出现过８．ｃ ｈ ｄ＾｛ｉｎ ｄ （ Ｈ ＾ｓｆ）；９．ａ ｄ ｄ Ｃｈ ｉ ｌ ｄ （ ｗ，ｃ／ ｉｔ〇；１ ０．｝１ １．ＥＬ ＳＥ ｛ 巧新的状态结点１ ２．ｃ ｒ ｅａ ｔ ｅＣｈ ｉｌ ｄ （ ｎ；１ ３ ．Ｈ． ｐ ｕｓｈ ｅ ｓ＇ｆｃ ｈｄ）； ｝１ ４．｝１ ５ ． ｝１ ６． Ｒ ＥＴ ＵＲＮｎ〇；算法ｉ 第一行初始化一个根靖点将：其存入到堆栈ｈ 中． 当堆栈不．为壑， 读出栈顶的结点》以及该錯点的状态Ｓ ． 箕法第６ 行遍历所有可以改变当前状态的事件ｅ ， 算法７ ？１ ３ 行将孩子状态加到当前结点的孩予集合中？ 第８ 行从Ｈ 中读出已有的一个结点第９ 行根据构造当前结点》的孩子． 第１ ２ 行根据Ｚ 构造ｍ 的一个新的孩子截獻回过头来分析例１ ， 这是“一手交钱４一＃交货”的经典交易模式？ 然而， 显熬例１ 是有问题的＊ 襄方＿全珥以在收到货款之唇不发货？ 在下一节＞我们将从博弈论的角度淹对例１ 进行分析， 并给出基于纳什均衡验测合同缺陷的方法，４ 智能合约的博弈问题商业合Ｗ是一个典型的博弈过程， 合同参与人在合同的不同状态上可遞有不同的策略， 以凝得对自己最有利的结果－ 举节将首弗定义智能合约的博弈问題， 再讨论如何基于博弈论的思想來負动分析合同的优劣．定义４ ． 智能含约博弈． 智能合约博弈由下列陈晋川等： 基于１ 期 纳什均衡 的智能合 约 缺陷检测 １ ５ ３部分组成：（ １ ）一个参与人的集合Ｎ ；（ ２ ）— 个状态变迁图Ｍ ＝（ Ｓ Ｃ ，《） ， 其中Ｓ Ｃ 是状态机（ 见定义３ ），《是参与人函数， 它赋给Ｓ Ｃ 中每个非终止状态￣■ 个参与人， 也就是指在非终止状态ｓ 上只有《〇） 可以采取行动；（ ３ ） 对每个参与人ｚ＇ｅ ｗ 有一个终止状态上的效用函数Ｍ， ：Ｒ ＋． Ｍ，〇） 表示参与人ｉ 在终止状态＾ £ ， 上的收益．图２ 中的例子也是一个状态变迁图． 包含两个参与人￣＝｛ 甲， 乙｝ ． 每个非终止状态（ 内部结点） 的行动人标在了结点旁边， 例如《（ Ａ ）＝ 甲． 参与人甲的效用函数是 Ｍ！  （ Ｄ）＝０ ， Ｍ！ （ Ｅ ）＝ １ ０ ， Ｍ！ （ Ｆ ）＝ １ ０ ０ ；参与人乙的效用函数是ｍ ２ （ Ｄ ）＝０， ｍ ２ （ Ｅ ）＝ １ ０，Ｍｚ （ Ｆ）＝１ ０ ０ ． 简略起见， 我们将两个参与人在一个终止状态的效用值写成一个向量． 在图２ 中， 结点Ｄ、Ｅ和Ｆ 下方是两个参与人的效用值， 甲在前， 乙在后．定义５ ． 智能合约博弈以，］＾ ＾ ， “ ） 〉＊ ＾ ，个参与人可以采取的策略集合是笛卡尔积ａ＝｛ｅ｜  （ ｓ ， ，ｅ ）— ｓ，ｅＺ ＼ ｝＿— 个策略组合是ｙ＝ （ ｏｎ ，…， （〇ｊ ｖ ） ｅ ｘ ， ｅ Ｎ ｆ ３， ， 其中（〇， ｅ ｆｔ 是参与人ｚ ｅｎ 策略集合的一个策略， 即第ｚ 个参与人在各个内部结点上所选择的动作．对于每个承诺《＾ ， ３ ＾， ＾ ， 「， 化） ， 责任方２ 是发出承诺的一方． 那么对于Ｃ ， 当前提ｆ 为真时， ：ｒ 就有两个选项， 履行承诺或者违约． 当前提ｆ 为假时，Ｚ 只有一个被动的动作选项， 即让承诺过期．例如， 图２ 中， 结点Ａ 对应承诺６ （ 伊， Ｚ ， ０ ，ｆ ａ＿ｙ （ Ｚ ， １ ０ ０ ） ， （ ⑵， ３ ） ） ． 由于前提条件恒为真， 甲在结点Ａ 上可以选择执行的动作为｛ｅｉ ，ｅ２ ｝ ， 即ｈ？ｅ 〇Ｍ ｉ＿６ ａ ５ （ Ｃ！ ） 和ｆ ａ＿ｙ ？ 第一■ 个动作表亦甲在约定期限内不付款， 使得该承诺违约． 第二个动作表示甲选择付款， 履行承诺． 因此在结点Ａ ， 甲的策略集合是ａ＝ ｛ｅｉ ，ｅ２ ｝． 类似地， 乙在结点Ｂ 可以执行的动作有｛ ｅ ３ ｝ ， 在结点Ｃ 可以执行的动作为｛ ｅ ４ ，ｅ ５ ｝ ． 那么乙的策略集合是笛卡尔积ａ＝｛ ｅ ３｝ Ｘ｛ ｅ ４ ，ｅ ５｝＝｛ｅ３ｅ４ ，ｅ３ｅ５ ｝ ？ 这里，ｅ３ｅ４ 是乙的一个策略， 含义是他在结点Ｂ 时会做动作ｅ３ ， 在结点Ｃ 会做动作ｅ４．参与人策略集合的笛卡尔积就是所有可能的策略组合集合． 例如， 根据甲和乙的策略集合， 有一个策略组合（ ６１ ，６３６４ ） ， 其含义是： 甲在结点４ 时会做动作＾ ， 乙在结点Ｂ 时会做动作ｅ３ ， 在结点Ｃ 时会做动作ｅ ４ ．对于每个策略组合７ ， 在状态变迁图中都能确定并且唯一确定一条从初始结点到终止结点的动作序列． 例如， 对于策略组合（ ｅｕ Ａ ｑ ） ， 在图２ 中Ａ 是初始状态， 甲做动作Ｑ ， 合约状态将改变为状态Ｂ ．按照策略组合的内容， 乙将在状态Ｂ 做动作ｅ ３ ， 合约将进人到终止状态Ｄ． 注意， 没有进人状态Ｃ ， 因此乙也就没有做动作？ 也就是说， 在一个策略组合中并非所有的策略都会真正执行．对于参与人来说， 他们的收益只与终止状态有关， 因此会关心动作序列的终止状态． 我们把动作序列表示为甲上乙：■ 〇， 其中Ｄ 是一个终止状态，甲Ｊ 表示参与人甲执行动作ｅ ｉ ．定义６ ． 智能合约博弈〈？ ， ］＾ ＾ ， （ 叫） 〉的策略形式表亦为〈Ｎ ， Ｍ ，） ， （ ｍ， ） 〉， 对于每个参与人有：（ １ ） ａ 是参与人ｚ＇ｅ ｗ 的策略集合；（ ２ ） Ｍ ｌ ： Ｘ ， ｅ Ｎ ［ａ — Ｒ＋ 是参与人ｚ 在策略组合上的效用函数． 任意一个策略组合Ｖ ｙ ｅ Ｘ ａ Ｎ ａ ， 在状态变迁图ｍ 中确定并唯一确定一条终止状态是ｓ的动作序列， 因此有＝〇） （ Ｍ ，〇） 是参与人ｉ在终止状态ｓ 上的效用） ．由于例１ 中只有两个参与人， 其博弈问题的策略形式可以通过效用矩阵表示（ 甲是行参与人，乙是列参与人） ， 如表１ 所示． 注意， 每个策略组合对应矩阵中一个元素． 例如， 策略组合（ ｅ ｉ ，ｅ ３ ｅ ４ ） 对应左上角的元素． 该策略组合在图２ 中确定了一条唯一的动作序列甲二乙二Ｄ． 因为有叫（ Ｄ ）＝０ 和ｍ２ （ Ｄ ）＝０ ， 左上角的效用值为（ ０ ， ０ ） ．表１ 效用矩阵甲－乙ｅ３ｅ４ｅ３ ｅ５０ ， ０ ０ ， ０ｅ２１ ０ ，１ ０ ｌ ｏｏ ａ ｏ ｏ定义７ ． 纳什均衡？ 智能合约博弈〈Ｎ ，Ｍ ，ａ，（ Ｍｌ） 〉的纳什均衡是一个策略组合ｙ＊＝Ｕ 『，…， 〇＾ ）ｅｘ ｉ ｅ Ｎ ｌＱ ， ， 使得对每个参与人ｗ ｅ ｗ 的策略ａ 有Ｍ，  （． ＣＵｔ ：ＣＵ ，  ）Ｍ ， （ （０ ， ５（０ ， ） ．上式中表示策略组合， 中去掉参与人Ｚ 的策略‘ 之后其他参与人的策略． （ 〇Ａ ， 〇０ 表示动作人Ｚ 选择任意策略， 其他参与人选择中规定的策略． 也就是对于任何一个参与者Ｚ 而言， 当其他每个参与者都选择均衡策略时， 参与者Ｚ 所有的策略产生的效用都不高于他选择策略Ｗ 所产生的效用．１ ５ ４ 计算机学报 ２ ０ ２ １年例如， 从表１ 中可以看到对双方都有利的策略组合是０ ２ ，ｅ３ｅ４ ） ， 在图２ 中对应着动作序列甲２ 乙Ｊ ｅ ， 含义是甲付款， 且乙发货， 双方各自可以得到１ ０ 的效用值． 然而， 这个策略组合不是一个纳什均衡， 因为乙可以改变他的策略为ｅ３ｅ５ ， 也就是不发货， 使得乙的效用值从１ 〇提高到１ ０ ０ ． 理性的乙在这种情况下会选择不发货， 因此甲付款且乙发货这样的理想局面无法出现． 根据表１ 可以计算出只有一个策略组合是纳什均衡， 即右上角的（ ｅ ｉ ， ｅ ３ ｅ ５ ） ．该策略组合在图２ 中对应着一条动作序列甲１ 乙ｉＤ ， 含义是甲不付款， 且乙不发货， 双方的效用值都是〇． 这是一个纳什均衡， 因为双方都无法通过单方面改变策略来获得更多的收益： 如果甲将他的策略改变为ｅ ２ ， 他的效用值会从０ 降低到 １ ０ ０； 如果乙将他的策略改变为ｅ３ｅ４ ， 他的效用值保持不变， 依然是〇．根据纳什均衡理论Ｈ１ ６ ］， 如果所有参与人都是理性的， 完全了解效用矩阵， 并且存在纳什均衡， 参与人会选择进人到纳什均衡的局面． 这是因为参与人在做策略选择时， 当预计到可能会进人到非纳什均衡的局面时，一些参与人知道他们可以通过改变策略获得更多的效用值． 由于他们都是理性的， 他们会改变策略， 因此非纳什均衡这个局面并不稳定． 由于存在纳什均衡， 这些参与人策略最终会收敛到纳什均衡策略， 因此会进人纳什均衡局面． 例如， 在前面的例子中， 假设甲乙都是理性的， 他们也知道表１ 的信息． 如果智能合约预计会进人到非纳什均衡局面０ ２ ，６３６４ ） ， 乙会将策略从６３６４ 改变到， 因为他的效用值会从１ ０ 提高到１ 〇〇， 但甲的效用值会从１ ０ 降低到 １ ０ ０ ． 但智能合约预计又会进人到另一个非纳什均衡局面（ ｅ２ ，ｅ３ｅ５ ） ， 甲又会将策略从＆ 改变到Ａ ， 因为他的效用值会从１ 〇〇提高到〇， 处于纳什均衡局面（ ｅ ｉ ，ｅ ３ ｅ ５ ） ， 也就是甲乙都选择不合作．当然， 现实情况中， 可能由于参与人的非理性行为或者不了解效用矩阵， 会进人到非纳什均衡的局面． 但本文考虑的是智能合约本身的问题， 因此假设参与人都是理性和完全了解信息的． 在前面例子中，甲乙只有选择不合作， 显然这样的智能合约是有逻辑缺陷的．定义８ ． 智能合约逻辑缺陷． 智能合约逻辑缺陷是一种使得参与人效用小于或等于零的纳什均衡ｆｅ， 也就是； 存在参与人ｅｎ ， 他从纳什均衡， 获得的效用小于或等于零， 即＆ （ ， ） ＜ ０ ．基于状态变迁图， 我们可以通过计算纳什均衡来识别出智能合约的逻辑缺陷， 然后自动分析出智能合约的优劣． 然而， 状态变迁图存在组合爆炸的问题． 图中的结点数量与合同中承诺数量成指数关系．当合同承诺数量较多时， 将难以得到分析结果． 接下来， 我们将讨论如何提高计算纳什均衡的效率， 这主要通过简化策略形式来实现．５ 策略形式的化简给定一个合约， 其策略形式本质上是状态变迁图中各个结点的策略集合得到的笛卡尔积． 因此， 对策略形式的化简， 首先考虑的是对状态变迁图进行化简． 此外， 我们还将讨论， 如何在生成策略形式时，避免生成冗余的策略组合．本节将首先介绍“ 等价策略” 合并原则， 在此基础上提出两个基于该原则的化简方法： 基于效用值相同叶结点的化简方法， 以及基于独立承诺的化简方法． 接下来， 我们将讨论一种新方法， 该方法可以突破等价策略的局限， 对状态变迁图进行进一步化简． 最后， 我们将提出一个发现冗余策略组合的方法， 避免一部分冗余策略组合的生成．５ ． １ 等价策略合并原则在经典的博弈论理论中［ ６ ］， 等价策略合并原则是最为常用的对策略形式进行化简的方法．定理１ ． 等价策略合并原则．一个策略形式〈？ ，］＾ ，（ 认），（ ＾０ 〉， 若对于某参与人々£ ？ 的两个策略（０丨和（０】，ｕ （ ｃｏ１＾ ｃｏ Ｎ ）＝ ｕ （ ｃｏ１， ＣＯＮ ） ，Ｍ （ｔ）ｔＧＯ ｔ （ ｉ即给定其他参与人的任何策略， 分别与Ｗ 和Ｗ构成的两个策略组合， 这两个策略组合的效用值对于每个参与人均相等． 注意： 对于一个策略组合ｙ＝（ ＣＯ ！ ，？ ？ ？， ＣＯ Ｎ ） ， Ｍ （ ｙ ）＝ （ Ｍ！ （＞〇，…， ＭＮ （＞０ ） 是一个ＪＶ 维向量， 表示所有参与人在策略组合ｙ 上的效用值．根据文献［ ６ ］ ， 若Ｗ 和Ｗ 满足上述条件， 则任何两个策略组合ｙ 和ｙ＇， 若Ｋ ｅ ｙ 且Ｗ ｅ ｙ＇， 则可以将７ 和， 合并为一个策略， 而不影响纳什均衡的计算．当只有两个参与人时， 上述条件成立等价于效用矩阵中有两个相同的行或列， 因此也可以将其称为“ 行（ 列） 相同合并原则接下来， 我们讨论利用这一原则对状态变迁图进行化简．離劑等Ｉ．霜１ 期 于靖计禅衡的臂俱脅约缺陷錄 １ ５ ５５ ． ２ 效用值相同叶结点合并方法定理２ ． 效用值相同叶结点合并规则． 若多个叶结袁１ ｘ４〃， ４ 属Ｔ 同一个非终止状态靖京的孩子， 且这些叶锘点上每个参与人的效用＾值都相等，》则将Ａ， 心合并将不擧响纳什均衡的求解，Ｍ 明． 东鬼一般性， 设参与人为甲， 设〇，？ ？ ？，Ｉ 分别为从父结点转移到込，…． ４ 的事件（ 也是甲的动作．） ？ ｖｙ ｅ：１，…， 假设ｙ， 和广为任鴦两个分别但當ｅ， 和９ 的策略摄合， 且ｙ，■ 和Ａ 除去ｅ， 和Ａ之外其余部：分完全相肩： ， 即ｙ， ／ｅ，＝乃／ ｑ ；若Ａ 和６ 在策略ｓ 合中均不生效（ 没肴包含在：对应的动作序列中） 和乃必然对应相同的执行路辏＊ 效用值相若為和￥有一个生效， 说明ｙ； 和ｙ， 对觀：的动作序列将到达Ｕ… 丄的父结点， 则私和＆／都会生效．因此ｙ， 和乃对處的动＇作療細必錐霉ｉｉ： 于？和％ 指向的叶结点， 效用値也相同， 因此ｙ； 和ｙ ，的效用值必然相等， 按等价＃ 略合并原则， 将ｙ， 和７， 合并将不影响纳什均衡的计算证毕．依据定理Ｌ 我们可以将ｆｌ３ 中左侧的两个叶结点予以合并．（ １ ０， １０ ）（ １ ０， １〇）（ １ ０， １ ０ ）图：ｓ僮相同叶鐘查翁行化＃ 的树子定理３ ． 内部勘ｉ 会并规剔． 碁多个肉部緖点赞１，？  ？ ， ） ＆封盧歸一个參％人， 它似均只有一个幾子结点， 且它们的孩子结点为同一．个奸结点， 则ａ ，…，篇？ 可以合同样不影响绡什均衡的求解，证明过程类似定理２ ， 限Ｔ 篤幅， 略去细节？依据定：理ｔ 我们可将图３ 中右侧图中倒数第二层的两个结点手以合并，Ｓ．３ 基于因果独立关系的化简方法１ 因果囊系和眉果：独立根据前面的分析． 我们知道例１ 的合约是存在漏洞的， 不利于建宜双方长期合作． 原因在于没有对乙的行为进行约束． 因此， 我们现在对例１ 进行完：善： 仿照支付宝和以太坊的思路， 加人鸯金盟眷． 购书款先存人到合约地址， 当乙履行发货义务》才将购书款转给乙？ 修改后的食钧承诺如下？例２ ． 第二版购书合同． 甲承诺在３ 天将书款１ ０ ０ 元存人到合约账户； 乙承诺在甲付款１ 天内发货； 甲承诺在乙发货７ 夫内确认收货ｆ Ｃｂ ｎｔ ｒｗｒ ｔ 承诺在甲确认收货１ 天构将书拿转账翁Ｋ〇：ｎｔ ｒ？ｔ ：素诺在； 乙违约（ 不发货． ） １ 天内将书款逭． Ｍ 给味．法套＇Ｃｏ ｎ ｔ ｒａｃ ｔ 的讀作暴智能合對代碎规：窠的，一旦前提满足， 就必然会执行， 因此Ｃｏ ｎｔ ａ ｃ ｔ 不会出现违釣．观察例２ 中的承诺， 我们可以发现一些承诺之间存吞依赖？ 比如． 承诺Ａ 的前提包含了Ｃ＼ ， 因此必须等ＣＶ 进人终來态之薛才能判断Ｃｒ是杳可以进人６ｋ 状态－ 下面， 我们引人因．枭关系的概念来描述这种依赖关篆．定义９ ．嵐果薦｛ Ｃａｒ ｓ ｓ ｌＧ ｒ ａｐ ｈ ） ， 给定一组癒诺ＣＣ ， 其相应的因果图Ｇ 定义如下：（ １）ＣＣ 中每一个承诺Ｃ，对座Ｇ 中一个顶京！（ ２） 如果一个承诺ｑ． 的前提中包含Ｃ； ， 侧在Ｇ中有一条有：向边从猎向ｑ ．．圏４ 麗示插是衡２ 中承：诺斯对遽的面果斷Ｃ＼ （＾ ，３ ？０ ？ ｄ ｅｐ ｏ ｓ ｉｌＣ Ｃｏｎ ｌｒ ａ ｃ Ｌ，１ ０ ０） ， （〇〇，３ ） ）Ｃ２＾ ｙ Ｃ＼． ｓａ ｉ －，ｄ ｅ ｌｉｖｅ ｒ （． ｂｏ ｏ ｋ －，， （ ３ ？ １ ） ）Ｃ３ （伊， 乙， 〇２ ． 犯“ ｃ ｏｗ／＾ｒ ｍ（ ｒ ｅ ｃｅｉ ｖ ｅ一ｂ ｏ ｏ ｋ） ， （ ７，７ ） ）Ｃ４ ｛． Ｃｏｎ Ｌｒａ ｃ Ｌ ． ｓ ａ ＬｙＬｒ ａｎ ｓｆｅ ｒ ｉ Ｚ ＾ １ ０ ０ｓ） ？ （ ３ ０？ １ ） ）Ｃ５ Ｃ Ｃｏｎ Ｌｒａ ｃ Ｌ＾ ＾ｙ Ｃｚ ． ｖｉ ｏ＾ｒ ｅｆｕｎｄ ＾１ ０ ０ｓ），  （ ３ ０，１ ） ）定义１ ０ ．震果養系（ Ｃａ ｒ ：ｓａｌ Ｒｅ ｌ ａ ｔｉ ｏ ｎ ） ， 給定两个承诺Ｃ， 和ＣＶ 定义Ｃ， 和Ａ ＃在因果潷系Ｓ 且仅当在因巣圈Ｇ 中存在至少一条路径连接ＣＶｆ Ｃ，． 若Ｇ 和Ｃ，不存在因果关系ｓ 我们称它们是國果独立Ｃｃａｒ ｇａｌ ｈｉ＜ｆｃｐｅ ｎｄ ｅ ｎｔ ） 的， 或’筒称猶立？注倉， 随翁合约的执行，某些承诺的状态可能发生改．变ｓ 若一个承诺Ｇ 进人某个绛止态， 我们须将＆对应的顶点和与萁相连的边都从Ｇ 中删除． 西此， 可能存在Ｃ； 和原本存在西果关系， 姐当含约执行到某个状态时它们变成了独立． 如图４ 所示，Ｃ４ 和Ｃ５ 本乘基＿ 在因：襄蘇系韵， 但如蔑ｑｒ遊人了终态並腿＇中驂去． 则ｃ４ 和＆独愈：＊１ ５ ６ 计導机攀报 ：＿１苹ｇ ． ３ ． ２ 黧会状态转「移若在茵果固＇中存在一条从Ｇ 到Ｃ， 的路径， 则Ｇ需要等待Ｇ 的执行结果才能发生状态改变， 但如果Ｃ； 和Ｃ， 是独立的． 则它们的状态改变可以以任意顺序发生． 例如． ． 膜设莲前合约状态为ｈ 弁痕设此时Ｃ， 和Ｃ， 都可以发生状态改变？ 假谗事件使得承诺Ｑ 发生致变Ｓ［ 起犹态转移＆ ：ｇＡ ）—幻， 使褥承诺々意生愈变， 并引起状态转移＆ ：ｙｔ也就是说， 通过状态转移序列可将合约状＿ 从Ｓ 转变到＆ ？ 同理， 若我们先玫变Ｃｒｒｌｆ 政变Ｃ ，， 也就是执行状态转移序列＆ 及，一样可以将合约状态从｜转变到上面的例予可Ｋ 看迅当相互独立的承诺发蛊状态敦变时， 我们可以将＿ 个状态玫蜜含舞到一起， 避免腾开不必粟的状态转移序列＿ ＿ 于状态变迁倒中一个结点只有一个动作人， 我们在合并状＿韓＿ ａ＃慕求被合＃ 的状寒转黪由據一？ 动作人发起．定义１ １ ． 复賣栽态：转務ｔＧ 〇ｍ ｂｉｎ；ｅ４ Ｔ Ｔｒ ａｕｓ ｉ ｔｉ ｐｕ ！ ）＇，设合约状态为ｓ ， 给定一组两两独立的承诺Ｇｍ＃ ｆ ￡； ？Ｋ俄ｋ ￡） ， 若參些承诺此时均能：翁生牧态改变． 不失一般性， 假设这些承诺依次改：变状态，产生的状蠢转穠＃ 列海蠢， ｉｎ…， ｓ：雜量终：得到合约状态且这些状态转移对应的事件分别为：Ｃ…Ｓ ６丄我们可以将这些状态转移合并为一个：ｆｔ合状翁转移咨？？ ［句：，為，…， ｅｍ ］ ）？ 这里，［ ？！ ， 咚，…］ 袭示途：饥个参：件的任蠢排列？需栗指出对于彳Ａ ， ｅ２，…， ｇｊ＊ ！＿任蠶＇— 个序列因为这些事件可以在状态ｓ 时独立发生， 其顺序不会影响结桌．虜５ 的左侧展示了根据例２ 承诺生．成的状态变迁图的一部分？ 可Ｋ１看到当Ｃｓ 进人如状态之后， Ｃ４和ＣＳｌ１ｆ 以独立改变自己状菰当事件ｆ ｍｗ／ｅ ｒ 发生， Ｃ ｉ从２ 歲靈到３； 当＿ 件ｉｉ ？柳ＣＧ ） 发生＞Ｇｒ从１ 玫：变：蘭ｔ 孤— 中苛以，看到， 这爾个攀件产生的苘个序列， ＿终得到相同的结果． 诨此， 我们可以将这两个状态转移合到右边的图．定理４ ． 基于复合状态转移的化简原则． 当状态变迕画的锫点＾ 存在一组两两独立的承诺■Ｉ  Ｃ！，…， 按窝义１ １ 将ｔ， 的多个状态转移路径合并太一个复合状态转本会影响纳什均衡的计算结果．证明． 设化简之前的状态变迀图为Ｃ； ， 通过一个复合状态转移＃ 对Ｇ 进行化商之后的状态变迁图为Ｇ ＇． 设ｙ 为任袁＾－十由Ｇ ＇ 生成且包含的策略组合？ 则ｙ 在＜３ 中对愈唯■一■ 条动作：豫到ｊ〇指向叶子结点夂其对应的效用？值为《■ （ ／） ？设在Ｇ 上对应的事件ｆ列集合为［ ， ］ ？ 并设Ｐ 在６ 上对应的路径菜合为Ｐ ．若不在Ｐ 上＞ 则任何屬于［ｅ？］ 的事？：件序列都不会出现在任何一条Ｐ 的路径上．署ｓ？ 在ｐ 上．， 则麗于［ ｅ？〕：的事秤零＿ 都在，Ｐ 的某条路径／／ 上． Ｐ 和／ 的畦一塞别在复合状态转移部分， 它们将指向相同的叶结点？ 也就是说， 包含这些序到的策略组合， 其效用值均为《（ ／ ） ．根据雩价策赂合并厳则可证．证毕．化简效果分析． 若一个状态Ｓ 包含Ａ 个独立承讀， 那歲未化筒前的状霧变：迁围将产生Ｈ： 个状态翁移序列， 钽是化简之后， 这幻个序列（ 路径） 将被合并为１ 个． 因此． 窟遲４ 可以大大减少状态变迀图．结点的数量， 也将大幅降低策略形式的数量．Ｓ． ４ 基于纳什均衡等价的化简方法之前讨论的化简方法的？础都Ｓ等价策略（ 行列相同１ 贪并原则． 但是等价策略合并不是方能的■菌６ （ ａ） 的例子中， 结点Ｃ 、Ｄ 、Ｅ 结构非常类似： 有柑同的父结蟲Ａ； 孩子結．点都是＿Ｆ 和：Ｇ ＊ 且转移到Ｆ或Ｇ 的夢件也相同． 我们着蓬将Ｃ、Ｄ 、￡合＃ 为一个结点， 如图６ ａ） 所示．（ ａ ） 原始图（ ｂ ） 化简图图Ｓ 我― 变ｔ？＝聲价图０ （ Ｓ） 的效用矩阵如表２ 所示ｃ羞中黑体部分为纳什均衡的策赂组合５ ． ■ 我们分析其效用矩阵时， 发现并不存在相同的行或列？ 无法适用Ｓ ， １ 小节里的等价策略原则（ 也就是行列合并原则） ．離劑等Ｉ．霜１ 期 于靖计禅衡的臂俱脅约缺陷錄 １ ５ ７表２ 图６ （： ａ３ 的效用矩阵乙甲ｅｉ ％ ｅ３ｅ４ｅ５ （ Ｃ） ｅ５  （ Ｄ ）ｅ５  （ Ｅ ） （ ４０，４ ０ ） （ ３ ０， ３ ０ ） （ ３ ０， ３ ０ ） （ ３ ０， ３ ０ ）ｅ５ （ Ｃ） ｅ５  （ Ｄ ）ｅ６  （ Ｅ ） （ ４ ０， ４ ０ ） （ ３ ０， ３ ０ ） （ ３ ０， ３ ０ ） （ ５ ０ ，５ ０ ）ｅ５（ Ｃ） ｅ６ （ Ｄ ）ｅ５ （ Ｅ ） （ ４ ０， ４ ０ ） （ ３ ０， ３ ０ ） （ ５ ０ ，５ ０ ） （ ３ ０， ３ ０ ）ｅ５（ Ｃ） ｅ６ （ Ｄ ）ｅ６ （ Ｅ ） （ ４ ０， ４ ０） （ ３ ０， ３ ６） （５ ０ ，５ ０ ） （５ ０ ，５ ０ ）ｅ６（ Ｃ） ｅ５ （ Ｄ ） ｅ５ （ Ｅ ） （ ４ ０， ４ ０） （５ ０ ，５ ０ ） （ ３ ０， ３ ０） （ ３ ０， ３ ０）ｅ６（ Ｃ） ｅ５ （ Ｄ ）ｅ６ （ Ｅ ） （ ４ ０， ４ ０） （５ ０ ，５ ０ ） （ ３ ０， ３ ０） （５ ０ ，５ ０ ）ｅ６（ Ｃ） ｅ６ （ Ｄ ） ｅ５ （ Ｅ ） （ ４ ０，４ ０） （５ ０，５ ０ ） （５ ０，５ ０ ） （ ３ ０，３ ０）ｅ６ （ Ｃ） ｅ６  （ Ｄ ）ｅ６  （ Ｅ ） （ ４ ０，４ ０ ） （ ５ ０，５ ０ ） （ ５ ０，５ ０ ） （ ５ ０，５ ０ ）但是我们规察化筒图的敏用矩阵， 发现一个有趣的现象．首先，，虽然不能适用行（ 列）相減会弁原则， 但是在： ＣＤＵ 二个總獻乙采取的策略是變金：相同的：选择则到达Ｆ ， 选择ｅ６ 则到达Ｇ ．其次，在化筒腾中得到两个策略组合＜＿ 中黑体标识）？ 如＿３ 所示＞ 其中左上角的策略组合！ｅ ５ 邊｝与表２ 左上角的策赂组合相同？ 在表２ 中该組合也齿傭什雄衡点． 右Ｔｆｌ 的策略組＃ ： ：， 炫｜ ｅ３｜ ｜ ｅ４ ｝其他部分保特，不变． 例如化简图中路径甲＾１＾ 乙上Ｇ， 对座原图三条路径， 甲Ｊ 乙上Ｇ， 甲上乙上Ｇ 和证明．（ ａ ） 设基于定理５ 的化简图计算得到纳什均衡点ｙ ， 且／ ．在化简＇ 图中对虛播径（〇． 将ｐ 中可翁翁作集％Ｉ Ｉ…１ １ ？ 拆开．， 可锝到原？ 中的路径集合八〈亨表示任翥动作序列） ？ 既然Ｉ Ｉ…ｌｋ？：ｋ） 满足纳什均衡条件， Ｖ 丨ｅ Ｕ 严，＿）， ｙ，＝亨． ｅ Ｉ：；ｅ丨也必然橋足．（＞ ４＝）Ｖ ／ Ｉ？ｉ２ ６１ １ ？． ＾＜＊， ｍ， ＼ｙ ， ｉ＝ｆｅ ａ ｅ］是纳什均衡處＃ 注意＇ｙ．ａＦｅ丨和； ２ｅ） 是＿＿京妒之后才分开， 不■ 妨假设的动作人为甲， 对乎甲在ｈ 的策略集， 其他人的最优策赂就基版棋？ 而和私》氣别仅银隹：擎私在敏点？＞？来取了《ｎ ， 而５％ ＿爾点采敢了《， ２．ｇ 为甲的焉詹动作均为它们的敏甩值是一样的， Ｍ 此， ７， ３也必然是纳什均銜点？ 这样我们就得到， ｌｌ ．－ ＇． ｍ ｝，含置：暴寧在ｅｇ 、ａ 或ｅ ４ 中任遨一个， 乙始终通择ｆｔ．可以遂一验证， 这个策略翁含与表２ 中标为黑体盆價綠ＣＪｆｌ ， ５ ０ ） 的１ ２ 个筆略龜合＝：是一致齒？ 比如！ｅ ６ （ Ｑ 物为甲选择了吟， 乙昀會—动作＿梟ｅ６ （ Ｓ＇；）， 也榦是：斑可歇筒化为１ ｅ６， ％ ｝．表３ 图６ （ ｂ３ 的效用矩阵乙甲＾１ｅｚｅ４它５ （４ ０，４ ０ ） （ ３ ０，３ ０）它６ （ ４ ０， ４ ０ ） （ ５ ０ ，５ ０ ）最后， ， 我们观察： ＾ ｊｂＩ ０４  １■ 所对应的执行路径（ ａ 中加粗的箭头所示） ， 该路径在遠图中对虛三条执行路径 ＜同＿遍加耝— 决＿獻５ ｆ餐身：讓征？ 这三条路ｆｔ对處的策路组合均为纳什均街点．基于以上观察， 我们提出以下基于纳什均衡等价的化简方法．定理５ ． 塞于纳什均衡等价的化简规．则． 若结處参合，？  ？ ？ ：ｓ％ Ｃｗ＞ １ ？：有＿一个父拿＿：蟲到，４＝ １，… 的动作分别为ｅ，： ； Ｖ 泛Ｕ ，…， 稱｝ ，ｖ潘翁乎＿嚴＿：合均为％ ，？  ＿ ＊ ；， ４（ 叶结處》，： 铒到ｊ（ｊ＝１ 、…， ＿ 动作为？ 且焉． 餘潘作执行人相隊？ 厕可将Ｗ 费并为一个绪点１？ 到》的：动作为ｆｔｉ Ｉ…｜ ｜ｕ， 到孩子象歲的儀作为ｇ ｆ说明： 依据定理５ 进行化筒， 我们将得到包含可选动作》例如趦卜， ｋ 的执行路径，，其在原图中对应坊个路轻？ 即将奐Ｉ…｜ ｜？拆开成单独的动作， 而７，＝ 砰＃；， 这些策略１１ 合要么都是纳什均衡点■． 么都不是纳什均衡点．若：策略癒脅藤ｔｙ，＝ｆ＆ｅｊＵ ＝１ ， ？抑！■：中每一个者Ｉ是纳什均衡虚， 容Ｓ曼出ｙ＝９？ ｔ％ 丨丨…Ｉ  ？？ ＞ ＊： 丨也必然满足纳什均衡条件，若策略组含集ｉ ｙ，＝ － Ｕ＝ １ ，…， ｗ ） 都不是纳什均衡点遍依据（ ４ ）猶遨否金题：， ｙ＝Ｙ （ ｅ ｉ｜ ｜…Ｉ ｅ，？  ） ｅ；＇也不＇可能是纳什均衡点，证毕．讨论：？ 经过上述化简， 状态转移图的规模大大缩小， 但是在基于状态转移图求纳什均衡的过程中依然遇到了很大问。题． 原因．在于求策略褒式过程中，＿票做两次笛卡命积． 揍下来， 我们将从另一个角度来简化策略形式， 即在＇构建策略组合时＊ 避免生成宂余＇餘麗合．Ｓ． Ｓ 冗余策略形式化简依据策略形式的＇定义， 我们瓣笋计算一个参与人在所有内部緒点的动作集合的笛卡尔积， 以得到谀参■ 与人所有策略． 例如獨甲的所有策略为＇！ 衛色％ 過％ ，１■， 即甲＿＜ ４ 的翁作：寒翁＇！  ？Ｊ， ｅ２｝嵐？＇冗余乘略藤式雛子１ ５ ８ 计導机攀报 ：＿１苹与他在Ｓ 的动作集合；， ｅ４ ｝ 做笛卡尔积．从画？ 中我们发现， 如果甲在锫点Ａ 选＃ ３＊ｅ２ ， 那么參作释．， 《＊ 必然不舍！生敏＊ 囡此■ ： 可能是冗佘的？ 基Ｔ 此观察， 我们提出卞肩的化筒方法？ＢＳ意到一个动作《实：顯对處狀盡变迁图隨一蠢斑， 为了便子播：述不翁设？■ 的源爾ｉｌ为（ ＜？ ） ， 目标翁森海定理６ ． 菪某动作人在：不同错点有两个策略為和暴抓（４ ） ＿ 祖先， 且，不在以ｒｆ ｓｔ （ ｅ ａ ）为根的矛树中， 则所有：同时＆ 貪（ 和４ 的倉略缀合都是冗佘的．证明． 假设一个策略親■含７ 同时包含￣和％ ．着ａ 生、效， 说明ｙ 对虛的路轻将经过边‘ ， 由于巧不在以办＞ 为根的子树中， 则今不可能生效．那么ｙ 可以被另一个吏短的策略组合ｙ ／ ，替代．若％４ 效， 说明ｙ 对应的路径将经过边峰， 则也不可能生效？ 那么ｙ 可以被另一个策略组合ｙ ／ ｃ眷代？着私和４均不生效， 则ｙ 可以被另一个策略组合ｙ ／＇！ 蜷％ 》餐代．综上所述． 任何同时包含＆ 和％ 的策略组合都是冗余的．证毕．实际应用中， 策略组含的数量可能非常大， 难以在短时间内全部构，造． 出来． 上述定：理：可以帮助我们避免＆ 成不必要的策略组令， 而不是在：生成所有策略＿合之唐再你筒，６ 系统实现和实验分析本节将首先介绍：我们开发的一个用于智能合约建模、分析以及部．署到Ｋ块链平台的工具， 接下来介靖我们对一组真实合同分析的结果， 以及我们所提出方隹在性能提升方面的表现．６ ． １ 系统介绍我饤开崖了一个用于智能合约建模、分析及自动部署的工具． ａ＆ 是部分截画？ （ ａ ） 麗示Ｔ一个合约的编辑界面， 用户可以输人合鈞的承诺、系统会自魂屣现承诸之间的依赖关系（ 因果依赖围ｈ（ ｂ＊） 展．示的是将一个合约負动部署到Ｆａｂ ｒｉ ｃ 平台的运行错果１（ｅ ） 是合约分析界．面《■ 用户可以看到根据合约承诺自＇动构建的状态变迀图， 在输人效用值之后， 还可以Ｓ 动分析合约的纳什均衡点， 其中黑色文字樞胰示了合约的一个执行路径？ 我们的工具还可以自动稂据状态变迕图生成智能合约的代码， 例如Ｈ ｙ－ｐｅｒ ｌ ｅｄｇ ｅｔ  Ｆ ａｂ ｒ ｉ ｃ 链码， 爾户：？其中鄯勢动作函数补充完＊：之后， 就可以使用我们的工具将含釣部署到Ｆａｌｉｒｉｃ 半舎上？ｔｒ ｖｃ，  ｔｃ ｋｅｎ－：？ ｃｙ ３－６ Ｃｃ ＊ｊ ？ｌ Ｊ ｒ Ｊ ＊Ｉ ｌ＇ ｆ． ：５ｌｎｉ ！ｃＣ Ｉ ５ ：Ｊ＜ ｐ ！ｒ 〇ｌ ］ ９ ．？ｙｎ ｅ Ｋｔ ＯＪＬ ＯＣ Ｔ ａｉ－ Ｎｓ Ｃｉｉ ！ ：？ ＣＡ Ｖ Ｈ ｌ Ｊ： ｊＤ ｉ＇ ＜Ｗ ｔ ＊ｌ ５ ｆ Ｖ ２ ？ｔ ｆ Ｚ Ｚ ｒＶ ：ｉ ｉｎ ｆ＞ ３ Ｊｎ ｈ ｉｆｔ Ｚ Ｓ ｌ＇ＪＩｋ ｉＨ Ｚ３ ｌ ５ ｌ ｒ，３ ｖ ｂ 〇ＬＨ Ｃ ｔ Ｊ＊２Ｃ ｌｐ ｒｆａ ｉ ｄ ｉｒａ ｒ ｊｎ ｖｊ Ｖ Ｔ ｒ ｎ Ｍ ｆ ｒ．  ＊＜ｍ ｉ ｉ＇； ｉ ｖｒｆ ｎ ｎ ／ｆｔ？ ｘ＿＇＞ ｎ ？ ． ｎ ｊ＊＿／ ｎ ｉ － １４ｊｎ ｉ ｉ ｒＣｉ ｉ ｉｉ Ｋ ｉＭ＇｝（ ａ ） 合约编辑 （ ｂ ） 合约部署我们采用了经典的Ｌｅｍｋ ｅ － Ｈｏ ｗｓｏｎ 算法［１ ５］ 来６． ２ 有效性实验求解纳什均衡．依据《中华人民共和国合同法》（ １ ９ ９ ９ 年３ 月１ ５ 日隊膂＿ 雩？．基于靖什埒衡的脊鱗脅舞缺騎翁興 ＩＳ  １ 期 ９颔布ｈ 常见的合同课有異卖含苘、供用杳同、赠与１合同等Ｉ Ｓ 粪？ 我们参照华律网（ ６ ６ ｋ ｗ． ｃｉ ｉ ） 和食同帮（上ｅｔｏｉｉ ｇ ｂ ． Ｃ ＤｌＡ） 爾，个网站齡合：＿審本＃ 使爾我们＇开衆的工具．＃其中１４ 类合同迸狞了建模和分析？Ａ有居间合Ｉｆ厨愈渉及到参方參与ｆ 暂时不变持．我们总计对１ ４ 大类．ＳＱ 个合同进行了建模和分析． 弁裉据分析结杲将这些含而分为Ｈ个等级？暑＾个纳什均衡点＊秦与各方敏用（ 收益：） 掬为＇零， 我们称为全零＾奢参与备＃效用均为正， 称为全定｜ 蓉有述有负， 称为ｆｉ负； 这三舞之外的｜３ｉｖ其你？如菌＆ 所每Ｖ在合同范本中ｓ 大部分含同质？量是合格的， 其中有３ ５ ％ 的食两达到了优秀？ 这些食同中， Ｈ 为只有全攀和全正的纳什均衡点ｒ參与＃方会优先考虑＇？＇双赢”的博弈策略，？ ｔ 纳什瑜衡正ｍｗｉ＿聋ｓ什均翁蟲麟鱗纖織崩Ｉ 会？ 分析＿＊姐我们也看到．， 有４ １ °４ 的含同存在丨可题． 这些含词中， 大部分是風存在全零的纳什均衡点？ 此时，參与．方在综食利弊之启， 将裉可能选择不參与博也就最不执行合屑．下面我们分析一个评分为４差” 的合同．合同实例： 清费寄托合＿Ｃ，＜ 申： 乙，， ｇｖ寄物品Ｈｆｔｆ寄托蠢＞（７ ，ｉ＞：）０２ （ Ｓ？ Ｃ， ．ａ？ｊ？ （，ｍ ， １ ３  ｉＧｒｆ；￡＊ 甲， 〇ｓ ， ｊ？， 薇用：青托物， Ｃ〇８？ Ｓ Ｄ ＸＪ＂（ 乙， ＿？忍： ．．》＃＆寄托满和天）！？ 退速： ｒ？ ））潸费寄托食同： 的含义是寧方将货物寄托在乙方处， 弁支付寄托金＊ 乙方可以在：寄托期间便用部分寄托物品（ 比如煤炭八隹是靖寄托期满， 乙方必摩ｆ 补足ＩＳ有物品數蒸＃妇还给甲方？上雄合约的含Ｘ慕； 甲方将物品寄托铪乙方并且付给．乙方ｓ偏〇■ 焉會托费ｆｄ．乙方决定备费爱颔寄托物（ ｃｙ ． 乙言可以自由消费寄托物（ ｃ＆ ） ，姐是必须．在寄托时间到期Ｃ＊ ： ／ ？＃ｅ 爾数调用预盲机实现） 后将脊．托物全额返．还给甲方．如果一开始甲方＇就将物品寄托＿ 乙方， 直方受？均为〇． 或者审方想要将物潘寄托给＆方是乙方木受领寄托物， 双方受益也均为０ ． 但是Ｓ寄托物一旦成功寄ｆｆｉ ｉｔ ｓ 乙方苜以自＿ 选择聲否执行？承诺ｃ４ ？ 如皋乙方违约， 不将寄托物返还给甲方， 这能使乙方自Ｈ 获傳更高的收益？輿此？ 上述合同Ｒ有全零的纳什均衡点， ￥如果逸择寄托物品， 那么作为理性的博弈参＝￥人， 乙将选择使ｇ 己收盘鱟大的策路＾违纨那么审在分析利弊之唐＊最好的对策甚？不哿托物品－ 也就意味：＃脅同根本本＇蠢裱执行？ 意獅奮獅到ｆ５緊方麓Ｓ健乘蕾要指出的是， 我们通过自：动分析，发现很多僉同范本都存在上述问题？ｊｔ有对某参省方的违约行为予以惩罚？ ＿ 么含同是杏：顺利执行可能Ａ有取决于该参与方的通禳水平或街律泝费？ 从商务合阏的原则来看， 这显潘是不合理的？可以＿ 出， 我们撻ｍ 的建镇方法賓ｍ＇对现实中大多数合同进行建模旦，基于傳弈论对合同自箭分析能够黛；现潛在雷逻辑缺陷（不公平的＊ 匣．６ ． ３ 效率实验我们按状态靖處数薫将合同分为吗类馮京载量分别为［ １ ＊孩〇］ ， ［ ５１ ， １０ ０ ］ ， ［ １１ １１， ２〇£ １ ＿ 茇［ ２： ０ １ｓｉ＃ ．状态緖点的数量讓本反腴了合词的复杂１程度．我们１对比了迪类：方法ｔ（ １ 〕ＤＦ Ａ 方：法＜奉用靈本的智能合约建模方法ｓ末做任何化简．（２ ３ ＳＥ方钹． 暴ｆ策略尋费（ ＳｔｒａｔｅｇｙＥｇｔ ｉｉ ｖａ：－ｌ ｅ ｆｉ＆ｅ．？， ＳＥ ）原则对状态变．迂图进行化简．⑶ ＳＥ ＋ Ｎ ￡方法． 莱用了ＳＥ 方法和纳什讀衡馨价攛则ｔｌ％ ｓ ｈ Ｅｃｊｕｉｍｌ？ｉｉｅｅ－； ｔＭ Ｕ） 封状盡变迁： 圈化简．ｆ ４３ ＳＥ ＋Ｗ Ｅ ＋ Ｒ Ｓ 方法？ 采用以上商：类化简方祛碁機上屈編用了５５南策略紙会化筒方掛ＣＲ ｅｄｕ ｎｄ ａ ｎｔＳｔ ｉａｔ ｅ ｇｙ？Ｒ Ｓ ） ＊下Ｗ我们分规从状态结處个数、策略级合个数以及计算纳什均衡时隊三ｔ 方爾验ｔｅ我们靳提出方麵有象性，ＩＱ 对比：了Ｄ ＦＩ ＳＥ ：和Ｓ Ｅ ＋ ＳＥ 这三种方＇法在四类合同中产生的状态緖点数量， 可见随着合闻趋宁复杂， 化简友法效果越明適． 特别地ｅ 爵杳同较为复杂， 化崎之后的结滅：栽量Ｒ 有化筒前的约１ 射．翁宁＃后一种化筒方铢（ Ｒ ｓ ｙ并不会减少状态録点个数， 我们没ｔ 在菌１〇中列出来．接下＿１ ， 我们猓人分折３种化简方法在计算纳什均衡过程中的效果《由子Ｉ５Ｆ Ａ 方法．只能计算出１ ６ ０ 计導机攀报 ：＿１苹１ ０ｓ１ ０＊１ ０３１ ０２１ ０１极少数＿ 常简攀費同的纳什均衡， 在窟綴分析中， 不再列出ＤＦ Ａ 方法的结果？厲＇１ １对比了ＳＥ： 、ＳＥ＋ＫＥ和ＳＥ ＋ ＮＥ＋ＲＳ 这三种方法：在四类合同中产生讷策略组合数量（ 对数藥标＞ ， 可以明显看到，嚴如了冗佘策略化简之．Ｓ ？策略组合数量明显下降， 对于复杂的合同， Ｓ Ｅ＋ ．ＫＥ＋ＲＳ 方法的策赂组合数比Ｓ Ｅ ＋ ＪｆＥ 方：法少了６ 个数量钣， 而Ｓ Ｅ 方法将会产生极多的策略组合， 以至ｆ根本不能在有敢时向内计算出纳什均衡．［ ０， ５ ０ ］［５ １，１ ０ ０］［１ ０ １ ， ２ ０ ０］［２ ０ １，■？］图１ ０ 狀态结啟个数１ 〇２。。１ 〇１ ５ ０１ ０？１ ０５。１０°□ＳＥ■ＳＥ＋ ＮＥ□ＳＥ＋ ＮＥ ＋Ｒ ＳＨ－］［０， ５ ０ ］［ ５ １， １ ００ ］［１ ０ １ ， ２ ０ ０］［ ２０ １ ，° °］丽：１１ 翁略组脅个数圈１ ２ 巖示了晦簾合同中ＳＥ、Ｓ Ｅ ＋ ＮＥ 和ＳＥ＋Ｊ Ｉ Ｅ＋Ｒ Ｓ 这兰种方法在计箅纳什均衡耗时的对比（ 对数垄标可以看到， 疊加了冗余策略化简之后，计算纳什均衡的效傘同样大幅提升． 对于一些非常复杂的合同， Ｓ Ｅ ＋ ＮＥ 方法＿要趙过一小时籴求纳什均衡， 而ＳＥ＋Ｎ Ｅ＋Ｒ Ｓ 方法只需要几秒， 我们在该：实验中设置的最长时间为ｌ ｈ ， 因此对宁Ｓ Ｅ 方法，其实际需要的时间远超过图中的数据．以上结果雇明， 我们所提出的化简方法． 可大幅度縮减计算纳什均衡所需的时间．７ 总结和展望区块链使用智能合约描述参与各方需要共同遵守的规则．一旦合约中存在漏洞问题， ！？往就会＇带来巨大的损失， 因此智能合釣缺陷检测成为了受到广泛关注的研穷向題■ 然而， 现在区块链的智能合钧并＇没有统一的编程语言和运行模型ｆ一般看寒由不檀计算机编程语言的管理人员负賣智能合约的创建和樟测？ 针对这个问题， 我们之前的‘工作提出了一种编程语ｉ 无关、易于：理解的智能合约模型／本文中， 在这个合约模複的基础上， 我们琅式化．定义了智能合釣的博弈问题， 然后提出基ｆ纳什均衡的漏洞检测方法〖并提出了一系列的策略濟式化简算法， 实前高效的缺陷检测． 此外， 我们实现了一个图琅化的工具， 可以对智能合约进行建模、分析和部署． 最后通过实ＩＩ 对方法的可，厨性和效率进行Ｔ 验ｉｔ＊末来我们将进一歩完德建模方法， 京持更复杂的语义． 也会研究基于机器、学习来求解纳什均衡的方法， 以支持實：为＇复杂的合同参考文献［ １ ］Ｓｚ ａｂ ｏ Ｎ． Ｓｍａ ｒｔ  ｃｏ ｎｔｒ ａ ｃｔｓ ：Ｂｕｉｌ ｄ ｉｎｇ  ｂ ｌ ｏ ｃｋｓ ｆ ｏ ｒ ｄ ｉ ｇ ｉｔ ａ ｌ ｍａ ｒｋ ｅｔ ｓ ．ＥＸ ＴＲＯ ＰＹ ： Ｔｈｅ Ｊｏ ｕ ｒ ｎ ａｌ  ｏ ｆ Ｔｒ ａｎ ｓ ｈｕｍ ａｎｉ ｓ ｔ Ｔｈｏ ｕ ｇ ｈｔ， １ ９ ９ ６，１ ６ ：［２ ］Ｌｕ ｕ Ｌ ， Ｃｈｕ Ｄ －Ｉ Ｉ ， Ｏ ｌｉ ｃｋｅ ｌ Ｉ Ｉ ， ｅｔ ａ ｌ ． Ｍａ ｋｉ ｎｇ ｓ ｍａｒ ｔ ｃｏ ｎｔ ｒ ａ ｃｔ ｓｓｍ ａｒ ｔｅ ｒ ／ ／ Ｐ ｒ ｏ ｃｅｅ ｄ ｉ ｎｇ ｓ  ｏ ｆ ｔ ｈｅＡＣＭ ＳＩ ＧＳ ＡＣＣｏ ｎｆ ｅｒ ｅ ｎｃｅ ｏ ｎＣｏ ｍｐ ｕ ｔ ｅｒ  ａｎｄ  Ｃｏ ｍｍｕ ｎ ｉ ｃａ ｔｉ ｏ ｎ ｓ Ｓｅ ｃｕ ｒ ｉ ｔｙ  （ ＣＣＳ’１ ６ ）． Ｖｉ ｅｎｎａ，Ａｕ ｓ ｔ ｒ ｉ ａ ，  ２ ０ １ ６ ：２ ５ ４ － ２ ６ ９［３ ］Ｍｉｎｉｓ ｔ ｒ ｙ ｏ ｆＩ ｎｄ ｕ ｓ ｔ ｒ ｙａｎｄＩ ｎｆ ｏ ｒｍ ａ ｔｉｏ ｎＴｅｃ ｈｎｏ ｌ ｏ ｇ ｙ ． Ｗ ｈｉｔｅＰ ａ ｐ ｅｒ ｏ ｎＣｈｉ ｎ ａ？ｓＢｌ ｏ ｃｋ ｃｈａ ｉ ｎ Ｔｅ ｃｈｎ ｏ ｌ ｏ ｇｙａ ｎｄＡｐ ｐ ｌ ｉ ｃａ ｔ ｉ ｏ ｎＤ ｅｖ ｅ ｌ ｏ ｐｍｅ ｎｔ，Ｏ ｃｔ ｏ ｂ ｅｒ  ２ ０ １ ６ （ ｉ ｎ Ｃｈｉ ｎｅ ｓ ｅ ）（工信部． 《中国区块链技术和运用发展白皮书》， ２ ０ １ ６ 年１ ０ 月）［４ ］Ｗ ａｎｇ Ｐ ｕ－Ｗ ｅｉ ， Ｙａｎｇ Ｉ ｌ ａ ｎｇ－Ｔｉ ａ ｎ ， Ｍｅ ｎｇ Ｊ ｉ ， ｅ ｔａ ｌ ． Ｆｏ ｒｍａ ｌｄ ｅ ｆｉ ｎｉ ｔｉ ｏ ｎｆ ｏ ｒ  ｃｌ ａ ｓ ｓ ｉ ｃａ ｌ ｓｍａ ｒ ｔｃｏ ｎ ｔｒ ａ ｃｔ ｓ ａ ｎｄ ｒ ｅｆ ｅ ｒ ｅｎｃｅ ｉｍｐ ｌ ｅ？ｍ ｅｎｔ ａ ｔｉｏｎ． Ｊｏ ｕ ｒ ｎａ ｌ ｏ ｆ Ｓｏ ｆｔ ｗａ ｒｅ ， ２０ １ ９，  ３ ０ （ ９ ） ： ２ ６ ０８－２ ６ １ ９ （ ｉ ｎＣｈｉ ｎｅｓ ｅ）（王璞巍， 杨航天， 孟佶等． 面向合同的智能合约的形式化定义及参考实现． 软件学报， ２ ０ １ ９，  ３ ０（９） ： ２ ６ ０ ８－２ ６ １ ９）［５ ］Ｄｅ ｓ ａｉ Ｎ， Ｃｈｏ ｐ ｒａ ＡＫ ，  Ｓｉ ｎｇ ｈＭ Ｐ． Ｒｅ ｐ ｒ ｅｓｅ ｎｔｉ ｎｇ  ａｎｄ ｒ ｅａｓ ｏ ｎｉ ｎｇａ ｂ ｏ ｕ ｔ ｃｏ ｍｍｉ ｔｍ ｅｎｔ ｓ  ｉｎ ｂ ｕ ｓ ｉ ｎ ｅｓ ｓ  ｐ ｒ ｏ ｃｅｓ ｓ ｅｓ ／ ／ Ｐ ｒ ｏ ｃｅｅ ｄｉ ｎｇ ｓ  ｏ ｆ ｔ ｈｅ２ ２ ｎｄ  ＡＡＡＩ Ｃｏ ｎ ｆｅ ｒ ｅｎ ｃｅ ｏ ｎＡｒ ｔｉｆｉ ｃｉ ａ ｌ  Ｉｎｔ ｅｌ ｌｉ ｇ ｅ ｎｃｅ． Ｖａ ｎｃｏ ｕ ｖｅ ｒ ，Ｃａ ｎａ ｄ ａ ，  ２ ０ ０ ７ ： １ ３ ２ ８－１ ３ ３ ３陈晋川等： 基于１ 期 纳什均衡的 智能合约缺 陷检测 １ ６ １［ ６ ］Ｏ ｓ ｂ ｏ ｒ ｎｅＭ Ｊ ， Ｒｕ ｂ ｉ ｎｓ ｔ ｅｉ ｎ Ａ． ＡＣｏ ｕ ｒ ｓ ｅｉ ｎＧａ ｍｅＴｈｅｏ ｒ ｙ ．ＵＳＡ ： ＭＩ Ｔ Ｐ ｒ ｅ ｓ ｓ，１ ９ ９ ４［ ７ ］Ｙａｎｇ Ｚ ， Ｌｅ ｉ Ｉ Ｉ ． Ｆｏ ｒｍａ ｌ ｐ ｒ ｏ ｃｅｓ ｓ ｖ ｉ ｒ ｔｕ ａｌ ｍａ ｃｈｉ ｎｅｆｏ ｒ ｓｍａ ｒ ｔｃｏ ｎｔ ｒ ａ ｃｔ ｓ ｖ ｅ ｒ ｉ ｆ ｉ ｃａ ｔｉ ｏ ｎ． Ｉ ｎｔ ｅｒ ｎ ａｔ ｉ ｏ ｎａ ｌ Ｊ ｏ ｕ ｒ ｎａ ｌ ｏ ｆ Ｐ ｅ ｒ ｆｏ ｒｍ ａｂ ｉ ｌ ｉ ｔｙＥｎｇ ｉ ｎｅ ｅｒ ｉ ｎｇ ，２ ０ １ ８，１ ４ （ ８ ） ： １ ７ ２ ６－ １ ７３ ４［ ８ ］Ｂｉ ｇ ｉ Ｇ， Ｂｒａ ｃｃｉ ａｌ ｉ  Ａ， Ｍｅ ａｃｃｉ Ｇ ，ｅｔ  ａｌ．Ｖａｌ ｉ ｄ ａｔ ｉ ｏｎ ｏ ｆ ｄ ｅｃｅｎｔ ｒａ ｌ ｉｚ ｅｄｓｍａ ｒ ｔ ｃ ｏ ｎｔ ｒａ ｃ ｔ ｓ ｔ ｈｒ ｏ ｕ ｇ ｈｇ ａ ｍｅ ｔ ｈｅｏ ｒ ｙ  ａｎｄ ｆ ｏ ｒｍａ ｌ  ｍｅｔ ｈｏ ｄ ｓ ／／Ｂｏ ｄ ｅ ｉ Ｃ ，Ｆｅｒ ｒ ａｒ ｉ  Ｇ， Ｐ ｒ ｉ ａｍ ｉ Ｃ ，ｅ ｄ ｓ ． Ｐ ｒｏ ｇ ｒ ａ ｍｍｉ ｎｇ Ｌａ ｎｇ ｕ ａ ｇ ｅｓｗｉ ｔ ｈＡｐ ｐ ｌ ｉ ｃａ ｔｉ ｏ ｎ ｓ ｔｏ Ｂｉ ｏ ｌ ｏ ｇ ｙ ａ ｎｄ Ｓｅ ｃｕ ｒ ｉ ｔ ｙ ， Ｌｅ ｃｔ ｕ ｒ ｅ Ｎｏ ｔｅ ｓ ｉ ｎＣｏｍ ｐ ｕ ｔ ｅｒ  Ｓｃ ｉ ｅｎ ｃｅ ９ ４ ６ ５ ．Ｃ ｈａｍ ： Ｓｐ ｒ ｉ ｎｇ ｅｒ， ２ ０ １ ５ ； １ ４ ２ － １ ６ １［ ９ ］Ｍａｖ ｒ ｉ ｄｏ ｕ  Ａ ＊Ｌａ ｓ ｚ ｋａＡ． Ｄｅ ｓ ｉ ｇ ｎｉ ｎｇ ｓ ｅ ｃｕ ｒ ｅＥｔ ｈｅ ｒ ｅｕｍ ｓｍａ ｒ ｔｃｏ ｎｔｒ ａ ｃｔ ｓ ： Ａｆｉ ｎｉ ｔ ｅ ｓ ｔ ａｔ ｅ ｍａ ｃｈｉ ｎｅ ｂ ａｓ ｅｄ ａ ｐ ｐ ｒ ｏ ａｃ ｈ／ ／Ｐ ｒ ｏ ｃｅｅ ｄ ｉ ｎｇ ｓｏｆ ｔ ｈｅ ２ ２ ｎｄ Ｉ ｎｔｅ ｒ ｎａ ｔｉ ｏ ｎａｌ Ｃｏ ｎｆ ｅｒ ｅｎｃ ｅｏ ｎＦｉ ｎａｎｃｉ ａ ｌ Ｃｒ ｙ ｐ ｔｏ ｇ ｒ ａｐ ｈｙａｎｄ Ｄ ａｔ ａ Ｓｅ ｃｕ ｒ ｉ ｔ ｙ （ ＦＣ２ ０ １ ８ ） ． Ｎｉ ｅ ｕｗｐ ｏ ｏ ｒ ｔ， Ｃｕ ｒ ａ ｃａ ｏ，  ２０ １ ８：５ ２３－ ５ ４ ０［ １ ０ ］Ｇａ ｏ Ｘ ， Ｓ ｉ ｎｇ ｈＭ Ｐ ．Ｅｘ ｔｒ ａ ｃｔ ｉ ｎｇ ｎｏ ｒｍ ａｔ ｉ ｖ ｅｒ ｅ ｌ ａ ｔ ｉｏ ｎｓ ｈｉ ｐ ｓ  ｆｒ ｏ ｍｂ ｕ ｓ ｉ ｎｅｓ ｓ ｃｏ ｎｔ ｒ ａｃ ｔｓ ／ ／Ｐ ｒ ｏ ｃｅｅ ｄ ｉｎ ｇ ｓ ｏ ｆ ｔ ｈｅ Ｉ ｎｔ ｅｒ ｎａｔ ｉｏｎａ ｌ Ｃｏ ｎｆｅｒ ｅｎｃｅｏｎ Ａｕ ｔ ｏ ｎｏ ｍｏ ｕ ｓ Ａｇ ｅｎｔ ｓ  ａ ｎｄ Ｍｕ ｌ ｔ ｉ ａ ｇ ｅｎ ｔ Ｓｙ ｓ ｔ ｅｍｓ  （ ＡＡＭＡＳ ） ．Ｐａ ｒ ｉ ｓ ， Ｆｒ ａ ｎｃｅ ， ２ ０ １ ４ ： １ ０ １－１ ０ ８［ １ １ ］Ｓｉ ｎｇｈ ＭＰ ， Ｃｈｏ ｐ ｒ ａＡＫ． Ｃｌ ｏ ｕ ｓ ｅａｕ ： Ｇｅｎｅｒ ａｔｉ ｎｇ ｃｏ ｍｍｕｎｉ ｃａｔ ｉｏ ｎｐ ｒ ｏ ｔｏ ｃｏ ｌ ｓｆ ｒ ｏ ｍｃｏ ｍｍ ｉ ｔ ｍｅｎ ｔｓ ／／ Ｐ ｒ ｏ ｃ ｅｅ ｄ ｉ ｎｇ ｓｏ ｆｔ ｈｅ３ ４ ｔｈＣｏ ｎｆｅ ｒ ｅ ｎｃｅｏ ｎ Ａｒ ｔ ｉｆｉ ｃｉ ａｌ Ｉｎ ｔｅ ｌ ｌｉ ｇ ｅ ｎｃｅ （ ＡＡＡＩ ） ．ＮｅｗＹｏ ｒ ｋ，ＵＳＡ ，  ２ ０ ２ ０［ １ ２ ］Ｄｅ ｓ ａｉ Ｎ ＊ Ｎａ ｒ ｅ ｎｄ ｒ ａ ＮＣ ， Ｓ ｉ ｎｇｈＭＰ ．Ｃｈｅｃ ｋｉ ｎｇ  ｃｏ ｒ ｒ ｅｃ ｔｎ ｅｓ ｓ  ｏ ｆｂ ｕ ｓ ｉ ｎｅ ｓ ｓ ｃｏ ｎｔ ｒ ａ ｃｔ ｓ ｖ ｉ ａ ｃｏ ｍｍｉ ｔ ｍｅ ｎｔ ｓ 一／Ｐ ｒ ｏ ｃｅ ｅｄ ｉ ｎｇ ｓ  ｏ ｆｔ ｈｅ ７ ｔ ｈＩ ｎｔ ｅ ｒ ｎａ ｔｉ ｏ ｎａ ｌ Ｊ ｏ ｉ ｎｔ Ｃｏ ｎｆ ｅｒ ｅ ｎｃｅ ｏ ｎＡｕ ｔ ｏ ｎｏ ｍｏ ｕ ｓ Ａｇ ｅ ｎｔ ｓ ａ ｎｄＭ ｕ ｌ ｔ ｉ ａｇ ｅ ｎｔ Ｓｙ ｓ ｔ ｅｍ ｓ （ ＡＡＭＡＳ２ ００ ８ ）．Ｅｓ ｔ ｏ ｒ ｉ ｌ ， Ｐ ｏ ｒ ｔ ｕ ｇ ａ ｌ ，２ ０ ０ ８ ： ７ ８ ７－ ７ ９４［ １ ３ ］Ｃｈｏ ｐ ｒ ａＡＫ ， Ｏ ｒ ｅｎ Ｎ ， Ｓｉ ｎｇ ｈ ＭＰ ，ｅ ｔ ａ ｌ ．Ａｎａ ｌ ｙ ｚｉ ｎｇ  ｃｏ ｎｔ ｒ ａ ｃｔｒ ｏ ｂ ｕ ｓ ｔ ｎｅ ｓ ｓ ｔ ｈｒ ｏ ｕ ｇ ｈ ａｍ ｏ ｄ ｅｌ  ｏ ｆ ｃｏ ｍｍ ｉ ｔｍ ｅｎｔ ｓ ／／ Ｐ ｒ ｏ ｃｅ ｅｄ ｉ ｎｇ ｓ  ｏｆｔ ｈｅ １ １ ｔ ｈＡＡＭＡＳ Ｉｎ ｔｅ ｒ ｎａ ｔｉ ｏ ｎａｌ Ｗ ｏ ｒ ｋ ｓ ｈｏ ｐ ｏ ｎＡｇ ｅｎｔ Ｏ ｒ ｉ ｅ ｎｔ ｅｄＳｏ ｆ ｔｗａｒ ｅ Ｅｎｇ ｉ ｎｅ ｅｒ ｉ ｎｇ （ ＡＯ ＳＥ） ．Ｂｅ ｒ ｌ ｉ ｎ， Ｇｅｒｍａ ｎｙ ， ２ ０ １ １ ： １ ７－ ３ ６［ １ ４ ］Ａｄ ｌ ｅｒ Ｊ ， Ｂｅｒ ｒ ｙ ｈ ｉ ｌ ｌ Ｒ ， Ｖｅｎ ｅｒ ｉ ｓ Ａ ，ｅ ｔ ａ ｌ ．Ａｓ ｔ ｒ ａ ｅａ ：Ａｄ ｅ ｃｅ ｎ？ｔ ｒ ａ ｌ ｉ ｚｅ ｄ ｂ ｌ ｏ ｃ ｋｃｈａ ｉ ｎ ｏ ｒ ａ ｃｌ ｅ／ ／ Ｐ ｒ ｏ ｃｅ ｅｄ ｉ ｎ ｇ ｓｏ ｆ ｔ ｈｅ２ ０ １ ８ Ｉ ＥＥＥＩ ｎｔ ｅ ｒ ｎａ ｔｉ ｏ ｎａ ｌ Ｃｏ ｎｆ ｅｒ ｅ ｎｃｅ ｏ ｎ Ｉ ｎｔｅ ｒ ｎｅ ｔ ｏ ｆ Ｔｈｉ ｎｇ ｓ （ ｉＴｈｉ ｎｇ ｓ ） ａ ｎｄＩ ＥＥＥ Ｇｒ ｅｅ ｎＣｏ ｍ ｐ ｕ ｔｉ ｎ ｇａ ｎｄＣｏ ｍｍ ｕ ｎｉ ｃａ ｔ ｉ ｏ ｎｓ  （ Ｇｒ ｅｅ ｎＣｏ ｍ ）ａ ｎｄ  ＩＥ ＥＥＣｙ ｂ ｅｒ，Ｐ ｈｙ ｓ ｉ ｃ ａｌ  ａｎｄ  Ｓｏ ｃｉ ａ ｌ Ｃｏ ｍｐ ｕ ｔｉ ｎ ｇ （ ＣＰ Ｓ Ｃｏｍ ）ａ ｎｄ  ＩＥ ＥＥＳ ｍａ ｒ ｔ Ｄ ａｔ ａ （ Ｓｍ ａ ｒ ｔＤ ａｔ ａ ） ． Ｈａ ｌ ｉ ｆａ ｘ， Ｃａｎａ ｄ ａ， ２ ０ １ ８：１ １ ４ ５ － １ １ ５ ２［ １ ５ ］Ｓ ｈａｐ ｌ ｅｙ  ＬＳ．Ａ ｎｏ ｔｅ ｏ ｎ ｔ ｈｅＬｅ ｍｋｅ－Ｉ Ｉｏ ｗｓ ｏ ｎａ ｌ ｇ ｏ ｒ ｉ ｔ ｈｍ／ ／Ｂａ ｌｉ ｎｓ ｋｉＭＬｅｄ ． Ｐｉ ｖｏ ｔｉ ｎｇａ ｎｄＥｘｔ ｅ ｎｓ ｉｏ ｎ ：Ｍａ ｔ ｈｅｍａ ｔ ｉ ｃａ ｌＰ ｒ ｏ ｇ ｒ ａ ｍｍｉ ｎｇ  Ｓｔ ｕ ｄ ｉ ｅ ｓ ？ ｖ ｏ ｌ１ ． Ｂｅ ｒ ｌｉ ｎ ， Ｇｅ ｒｍａ ｎｙ ： Ｓｐ ｒ ｉ ｎｇ ｅ ｒ ，２ ０ ０ ９［ １ ６］Ｓ ｕ ｒ ｅｋ ａ Ａ， Ｗ ｕ ｒｍ ａｎＰ Ｒ ． Ｕｓ ｉ ｎｇ Ｔａｂ ｕ  ｂ ｅ ｓ ｔ－ｒ ｅ ｓ ｐ ｏ ｎｓ ｅｓ ｅ ａ ｒ ｃｈｔ ｏｆｉ ｎｄ ｐ ｕ ｒ ｅ ｓ ｔ ｒ ａｔ ｅ ｇｙ Ｎａ ｓ ｈ ｅ ｑ ｕ ｉｌｉ ｂ ｒ ｉ ａ ｉ ｎ ｎｏ ｒｍａ ｌ ｆｏ ｒｍ ｇ ａ ｍｅ ｓ ／ ／Ｐ ｒ ｏ ｃｅ ｅｄ ｉ ｎｇ ｓ ｏ ｆ ｔｈ ｅ４ ｔ ｈＩ ｎｔ ｅｒ ｎａｔ ｉｏ ｎａ ｌＪｏｉ ｎｔ Ｃｏ ｎｆ ｅｒ ｅ ｎｃｅ ｏ ｎＡｕ ｔ ｏ ｎｏｍ ｏｕ ｓ Ａｇ ｅｎ ｔｓ  ａｎｄ Ｍｕ ｌ ｔ ｉ ａｇ ｅｎｔ  Ｓｙ ｓ ｔ ｅｍｓ  （ ＡＡ ＭＡＳ２ ０ ０ ５ ） ．Ｕ ｔｒ ｅｃｈ ｔ ， ＴｈｅＮｅ ｔ ｈｅｒ ｌ ａ ｎｄ ｓ ＊ ２ ０ ０ ５ ： １ ０ ２３－１ ０ ２ ９ＣＨＥ Ｎ Ｊｉｎ－Ｃ ｈ ｕａｎ ， Ｐｈ． Ｄ． ，ａ ｓ ｓ ｏｃｉ ａ ｔ ｅｐ ｒｏｆｅ ｓ ｓｏ ｒ．Ｈｉｓ ｍａ ｉｎｒ ｅｓ ｅ ａ ｒｃ ｈ ｉ ｎｔ ｅ ｒｅ ｓ ｔ ｓｉｎ ｃ ｌｕｄ ｅ ｄｉｓｔ ｒｉ ｂｕ ｔ ｅｄ  ｄａ ｔ ａ ｍａｎａ ｇ ｅｍｅ ｎｔ  ａｎ ｄｂ ｌｏ ｃｋ ｃ ｈ ａ ｉｎ．ＸＩ ＡＨｕ ａ－Ｈｕ ｉ， Ｍ．  Ｓ．ｃ ａｎ ｄｉ ｄａ ｔ ｅ．Ｈ ｉｓｍａ ｉｎ ｒ ｅ ｓ ｅａ ｒ ｃ ｈｉｎ ｔ ｅ ｒｅ ｓ ｔ ｓ ｉｎ ｃｌ ｕ ｄｅ ｂ ｌｏ ｃ ｋｃ ｈ ａ ｉｎ  ａｎ ｄｓ ｍａ ｒｔ ｃ ｏ ｎｔ ｒ ａ ｃ ｔ ｓ．ＷＡＮＧＰｕ －Ｗｅ ｉ， Ｐ ｈ ．Ｄ． ， ａ ｓ ｓｏ ｃｉ ａ ｔ ｅｐ ｒｏ ｆｅ ｓｓ ｏ ｒ．Ｈ ｉｓ ｍａ ｉｎＢ ａｃｋｇｒ ｏｕｎｄＴｈ ｉ ｓ ｗｏ ｒｋ ｆｏ ｃｕ ｓ ｅ ｓｏ ｎ ｔｈ ｅ ｐ ｒｏ ｂｌ ｅｍｏｆ ｍｏｄ ｅ ｌｌ ｉｎ ｇａ ｎｄａｎａ ｌ ｙｚ ｉｎ ｇｓ ｍａ ｒ ｔ ｃ ｏ ｎｔ ｒ ａ ｃ ｔ ｓ ． Ｒｅ ｃ ｅ ｎｔ ｙ ｅａ ｒ ｓ ， ｓ ｍａ ｒ ｔ ｃｏ ｎ ｔ ｒａ ｃ ｔ ｓ ａ ｎｄｂｌ ｏｃ ｋ ｃ ｈａ ｉ ｎｂ ｅ ｃ ｏｍｅ ａ ｈ ｏｔ ｒ ｅ ｓｅ ａ ｒ ｃ ｈｔ ｏ ｐｉ ｃ ｉｎ ｄ ｉ ｓ ｔ ｒ ｉ ｂ ｕｔ ｅｄ ｃｏ ｍｐ ｕ？ｔｉｎ ｇ ，ｉｎ ｆｏｒ ｍａ ｔｉ ｏｎ  ｓ ｅ ｃｕ ｒｉｔ ｙ ， ｄ ａ ｔ ａ ｂ ａ ｓ ｅ， ａ ｎｄｓ ｅ ｒ ｖｉｃ ｅ  ｃｏ ｍｐｕ ｔｉ ｎｇｅ ｔ ｃ． Ｍｏ ｓｔ ｗｏ ｒ ｋｓ  ｒｅ ｇａ ｒ ｄ ｓ ｍａ ｒｔ  ｃ ｏｎ ｔ ｒａ ｃ ｔ  ａ ｓ ｃ ｏｍｐ ｕｔ ｅｒ ｐｒｏ ｇｒ ａｍｓｒｕ ｎ ｎｉｎ ｇｏ ｎ ｂｌ ｏｃ ｋ ｃ ｈａ ｉ ｎ ｓｙ ｓｔ ｅｍｓ． Ｈ ｅｎ ｃ ｅ ｔｈ ｅｓ ｅ ｓ ｍａ ｒｔ  ｃｏ ｎ ｔ ｒａ ｃ ｔ ｓｈａ ｖ ｅ ｎｏ ｔｈ ｉｎ ｇ ｔｏｄ ｏｗｉ ｔｈ “ｃｏ ｎ ｔ ｒａ ｃ ｔ ｓ Ｏ ｕｒ ｗｏ ｒ ｋｔ ｒ ｉ ｅ ｓ ｔ ｏｂｒ ｉ ｄｇｅ ｔｈ ｅ ｇ ａ ｐ ｂｅ ｔｗｅ ｅ ｎｂ ｕｓ ｉｎ ｅ ｓ ｓｃ ｏｎ ｔ ｒ ａ ｃｔ ｓ ａｎ ｄｃｏ ｍｐ ｕｔ ｅ ｒｃｏ ｄ ｅｓ．Ｍｏｒ ｅｏ ｖ ｅｒ，ｉｎｔ ｈｅ ｍｕｌ ｔｉ－ ａ ｇｅ ｎｔ ｃｏ ｍｍｕｎ ｉｔ ｙ ｔｈ ｅｒ ｅ ｈａ ｖｅｂ ｅｅ ｎ ｍａｎ ｙｗｏｒ ｋｓ ｏ ｎｍｏ ｄｅ ｌｌ ｉｎ ｇ ｂｕ ｓｉｎ ｅ ｓ ｓｃ ｏ ｎｔ ｒ ａ ｃｔ ｓ， ｏｒｉｎ ｔ ｅ ｒ－ ｏｒ ｇａ ｎｉ ｚａ ｔ ｉ ｏ ｎｐｒ ｏｃ ｅ ｓ ｓｅ ｓ ．Ｍｏ ｓｔ  ｏｆ ｔｈ ｅ ｓ ｅｗｏｒ ｋｓ ａ ｒ ｅ ｂ ａ ｓ ｅｄｏｎ ｔｈ ｅ ｃｏｍ ｍｉ ｔｍｅ ｎ ｔｍｏ ｄｅ ｌ ． Ｔｈ ｅ ｙｔ ｒ ｙｔ ｏｄ ｅｓ ｃ ｒ ｉ ｂ ｅｂ ｕ ｓｉ ｎｅ ｓ ｓｃｏ ｎ ｔ ｒａ ｃ ｔ ｓ ｗｉｔｈｆｏ ｒｍａ ｌ ｍｏ ｄｅ ｌ ｓ，ａｎ ａ ｌｙ ｚ ｅ ｔｈ ｅ ｃ ｏｒｒ ｅ ｃ ｔｎ ｅｓ ｓ ｏ ｆｔｈ ｅｐｒ ｏｐ ｏｓ ｅ ｄｍｏｄ ｅｌ ｓ，ａ ｎｄ ｄ ｉｓ ｃｕ ｓ ｓ ｈｏ ｗ ｔ ｏｕｔｉ ｌ ｉｚ ｅ ｔｈ ｅｍｏｄ ｅ ｌｓ ｔ ｏｓｉｍｕｌ ａ ｔ ｅ ｔｈ ｅｐｒ ｏｃ ｅ ｓ ｓ ｅｓ ｏｆ ｅ ｘｅ ｃ ｕｔｉｎｇ ｂ ｕｓｉ ｎｅ ｓ ｓ ｃｏ ｎｔ ｒａ ｃ ｔ ｓ．ｒ ｅ ｓ ｅａ ｒ ｃ ｈｉ ｎｔ ｅｒ ｅ ｓ ｔ ｓｉ ｎｃ ｌ ｕｄ ｅ ｓ ｅｒ ｖｉｃ ｅｃ ｏｍ ｐｕ ｔｉｎ ｇａ ｎｄ ｂｌ ｏｃ ｋ ｃ ｈａ ｉ ｎ．ＭＡ Ｎａ－Ｂ ｏ ， Ｍ． Ｓ．ｃ ａｎｄｉ ｄ ａｔ ｅ． Ｈｉｓ ｍａ ｉｎ ｒｅ ｓ ｅａ ｒｃ ｈｉｎ ｔ ｅｒ ｅｓ ｔｓｉ ｎｃ ｌ ｕｄ ｅ ｄｉｓｔ ｒｉ ｂ ｕ ｔ ｅ ｄｃ ｏｍｐ ｕ ｔｉｎ ｇａｎ ｄ ｂｌ ｏｃ ｋ ｃｈ ａ ｉｎ．ＷＡＮＧＱｉ，Ｍ．Ｓ． ｃ ａｎ ｄｉ ｄａ ｔ ｅ． Ｈｅ ｒｍａ ｉ ｎ ｒ ｅｓ ｅ ａ ｒｃ ｈ  ｉｎ ｔ ｅ ｒｅ ｓ ｔｉ ｓｂ ｌｏ ｃ ｋ ｃｈ ａ ｉ ｎ．ＬＩ Ｈａｏ－ Ｒａｎ， Ｍ． Ｓ ．ｃａｎｄ ｉ ｄａ ｔ ｅ． Ｈｉ ｓｍａｉ ｎｒ ｅｓ ｅａ ｒｃ ｈ ｉｎ ｔ ｅｒ ｅｓ ｔｓｉ ｎｃ ｌ ｕｄ ｅ ｓ ｅｒ ｖｉｃ ｅｃ ｏｍ ｐｕ ｔｉｎ ｇａｎ ｄ ｂｌ ｏｃ ｋ ｃｈ ａ ｉ ｎ．ＤＵ Ｘｉ ａｏ －Ｙｏｎｇ ， Ｐｈ ． Ｄ． ， ｐｒ ｏｆｅ ｓ ｓ ｏｒ． Ｈｉｓ ｍａ ｉｎ ｒ ｅｓ ｅ ａ ｒｃ ｈｉ ｎｔ ｅｒ ｅ ｓｔ ｓｉ ｎｃ ｌ ｕｄ ｅ ｄｉｓｔ ｒｉ ｂ ｕ ｔ ｅ ｄｄ ａ ｔ ａ ｍａｎａ ｇ ｅｍｅ ｎｔ ｔ ｅ ｃｈ ｎ ｏｌ ｏｇｙ ．Ｄｉ ｆｆ ｅｒ ｅ ｎｔ ｆｒ ｏｍｔ ｈ ｅｓ ｅ ｗｏ ｒｋ ｓ ， ｔｈ ｅ ｅｍｐ ｈａ ｓ ｉ ｓ  ｏｆ ｔｈ ｉ ｓｐ ａ ｐ ｅｒｉ ｓ ａ ｂｏ ｕｔｈｏ ｗｔ ｏａｎ ａ ｌｙ ｚｅ  ｔｈ ｅ ｌｏ ｏｐ ｈｏ ｌ ｅｓ ｏ ｆ ｃｏ ｎｔ ｒ ａ ｃ ｔ ｓ ． Ｆｏｒｔｈ ｉ ｓ ｐｕ ｒ ｐｏ ｓ ｅ，ｗｅ ｐｒ ｏｐ ｏｓ ｅ ａｍｅ ｔｈｏ ｄ ｔ ｏｃ ｏｍｐ ｕｔ ｅ ｔｈ ｅ Ｎａ ｓ ｈｅ ｑｕ ｉｌｉ ｂ ｒｉｕ ｍｓｏ ｆｆｏ ｒｍａ ｌｉｚ ｅ ｄ ｃｏ ｎｔ ｒ ａ ｃｔ ｓ ａｎ ｄ ａ ｓ ｅｒｉｅ ｓ ｏｆ ｔ ｅ ｃｈ ｎｉ ｑｕ ｅｓｔ ｏｓ ｐ ｅ ｅｄ ｕ ｐｔ ｈｉｓｐ ｒｏ ｃ ｅ ｓｓ． Ｔ ｏｔｈ ｅ ｂｅ ｓ ｔ  ｏｆ ｏ ｕｒ ｋ ｎｏ ｗｌ ｅｄ ｇ ｅ，ｔｈ ｉｓｗｏ ｒｋ ｉｓｔｈ ｅ ｆｉｒ ｓ ｔ ｏ ｎｅ  ｔｈａ ｔｉ ｌ ｌｕ ｓ ｔ ｒａ ｔ ｅ ｓａｐ ｒａ ｃ ｔｉｃ ａ ｌ ｐ ｒｏ ｃ ｅ ｓｓ ｔｏｄｅ ｔ ｅｃ ｔ  ｌｏ ｏｐ ｈ ｏｌ ｅ ｓ ｏｆ ｂ ｕｓ ｉ ｎｅ ｓ ｓｃ ｏ ｎｔ ｒ ａ ｃｔ ｓｂ ａ ｓ ｅ ｄｏ ｎ Ｇ ａｍｅ ｔｈ ｅ ｏｒ ｙ．Ｔｈ ｉ ｓ ｉ ｓ ｔｈ ｅ ｎ ｅｗｅ ｓ ｔ ｒｅ ｓ ｕ ｌｔ ｏ ｆ ｏｕ ｒｒ ｅ ｓｅ ａ ｒ ｃ ｈ． Ｐｒ ｅｖ ｉ ｏ ｕｓ ｗｏｒ ｋｓ ｏｎｔｈ ｉｓ ｔ ｏ ｐｉｃｈ ａ ｖ ｅ ｂｅ ｅ ｎ ｐ ｕｂ ｌｉｓ ｈ ｅｄ ｉ ｎＩＣＳＥ ， Ｔ ＰＤＳ ， Ｊ ｏｕ ｒｎ ａ ｌｏ ｆＳｏ ｆｔｗａ ｒｅ  （ ｉｎ Ｃｈ ｉｎ ｅ ｓ ｅ ）ｅ ｔ ｃ．Ｔｈ ｉｓ ｗｏｒ ｋｉｓｓ ｕ ｐ ｐｏ ｒｔ ｅ ｄ ｂ ｙｔｈｅ Ｎａ ｔｉ ｏｎ ａ ｌ Ｎａ ｔ ｕｒ ａ ｌ Ｓｃｉｅ ｎｃ ｅＦｏ ｕｎ ｄａ ｔ ｉ ｏｎ  ｏｆ Ｃｈ ｉｎ ａ （ Ｎｏ． Ｕ１ ９ １ １ ２ ０ ３ ） ， ａｎｄ ｔｈ ｅ ｊｏ ｉｎ ｔｐ ｒｏｊｅｃ ｔ ｓｆｒｏ ｍ Ｇｕ ｉ ｚ ｈｏ ｕＣｏｌ ｌ ｅｇ ｅ ｏｆＦ ｉｎ ａｎｃ ｅ  ａｎｄ Ｅｃ ｏｎ ｏｍｉ ｃ ｓａｎ ｄ Ｃｈｉ ｎｅ ｓ ｅＡｃａ ｄ ｅｍｙｏｆ Ｉｎ ｔ ｅ ｒｎ ａ ｔｉ ｏ ｎａ ｌ Ｔ ｒａ ｄ ｅ ａｎ ｄＥｃ ｏｎ ｏｍｉｃ ｓＣｏｏｐ ｅ ｒａ ｔｉ ｏｎ（ Ｎｏ． ２ ０ １ ７ ＳＷ Ｂ ＺＤ ０ ８ ） ．