基于博弈的电子商务协议分析

《基于博弈的电子商务协议分析》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、万方数据第27卷第3期2006年3月通信学报JoumalonCo舳unicationsVbl．27No．3March2006基于博弈的电子商务协议分析文静华1，一，张梅1，李祥2(1．贵州财经学院信息学院，贵州贵阳550004；2．贵州大学计算机软件与理论研究所，贵州贵阳550025)摘要：提出用一种新的基于博弈的逻辑方法分析电子商务协议，克服了传统时序逻辑把协议看成封闭系统进行分析的缺点。新方法可以成功地对电子商务中的对抗与合作行为进行描述，能够分析协议的保密性、安全性、非否认性及公平性等。最后用新方法对zhou．Golhn龃n协议进行了严格的形式化分析。结

2、果表明基于博弈的A几逻辑比传统的基于计算树逻辑(cTL)更适合于描述和分析复杂电子商务协议。关键词：电子商务协议；安全性；公平性；A几中图分类号：TP309文献标识码：A文章编号：1000．436x(2006)03。0073．061一■●●●■J●■1量I。0rmaIanalySlSOIe-C0mmerCeprot0C0lSDaSen0ngame、ⅣENJing-hualp，ZHANGMeil，LIXi觚92(1．Infb咖ationInstitutc，GuizhouFin强cialInstitute，Guiy卸g550004，China：2．Institut

3、eofSoftware卸dTheo啦GuizllouUniVc璐ity’Guiy柚g550025，China)Abstract：Anewlogicalmettlodbasedong锄etoaIlalyzee—commercepmtocolswaspmposed，meshortcomingof仃a—ditionaltemporallogicttlatrcgardspmtocolsasclosesystemto锄alyzehadbcenoVerc姗e．TheadVers撕al锄dcollabomtioninelec臼onicco姗ercecouldbedescri

4、b。dcorrectlybyttlenewmenlod，andmepriVacy'securi劬non·repudialion，胁messcouldbe锄aly髓d．Intlleend，strictf0】[1I】融柚alysisfbrZhou-Gollm龃nprotocolwasmadebytllenewmetllod．Theseworksindicatemattllealtemating-dmetemporallogic(ArL)lo百cbasedongameismoresuit-abletodescribe锄dallalyzeco唧lexe-commerc

5、epmtocolsman缸钮ditionalCTL-KeywoHIs：e—coI砌ercepmtocols；security；faimess；ATL1引言随着电子商务在Intemet上的日益盛行，网络和电子商务的广泛应用给人们的工作和生活带来了极大的方便。而电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础，这类协议的基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性等11’2J。同其它密码协议一样，电子商务协议的建模与形式化分析研究非常重要，对于已成熟的密码协议分析技术可以直接应用到电子商务协议中去。可以通过

6、用电子商务协议的形式化研究结果去指导电子商务协议的设计或弥补原协议中的潜在问题【3．4】。因此，进行电子商务协议的形式化分析与验证研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。基于时序逻辑的密码协议(包括电子商务协议)形式化分析方法已成为一个研究热点13娟J，其收稿日期：2005．07．26；修回日期：2006．01．09基金项目：贵州省科学技术基金资助项目(20052111)；贵州省教育厅自然科学基金资助项目(2004219)Fo咖da60nI把腿：mGuizhouScie眦eFoundadonofCllinaunderG啪t(20

7、052“1)：neGu油ouEduc觚onNaturalSci即ceFbundationofCtlinaunderG啪t(2004219)万方数据通信学报第27卷中，Emerson等人提出的线性时序逻辑(L1工)方法15】具有很强的描述能力，可以对协议系统进行形式化建模分析并开发了相应的检测工具sPIN进行自动验证，得到了广泛应用；Clarke和EInerson在LTL基础上提出了基于计算树逻辑(CTL)【7】的协议分析验证方法，能够对协议的并发性质进行更为准确的描述，同时也开发了自动模型检测工具SMV与NuSMv。这些传统时序逻辑方法由于把协议看成封闭式并发

8、系统进行研究，不能有效描述协议与外部环