基于atl的公平电子商务协议形式化分析

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

1、万方数据第29卷第4期2007年4月电子与信息学报JotlrnalofElectronics&Information，11echn0109yVbl_29No．4Apr．2007基于ATL的公平电子商务协议形式化分析文静华①②③李祥①张焕国②梁敏③张梅③①(贵州大学计算机软件与理论研究所贵阳550025)②(武汉大学计算机学院武汉430072)③(贵州财经学院信息学院贵阳550004)摘要：针对传统时序逻辑【TL，CTL及CTL4等把协议看成封闭系统进行分析的缺点，Kremer博士(2003)提出

2、用一种基于博弈的ATL(Alternatin争timeTempormLogic)方法分析公平电子商务协议并对几个典型的协议进行了公平性等方面的形式化分析。本文讨论了ATL逻辑及其在电子商务协议形式化分析中的应用，进一步扩展了Kremer博士的方法，使之在考虑公平性等特性的同时能够分析协议的安全性。最后本文用新方法对zhou等人(1999)提出的zDB协议进行了严格的形式化分析，结果发现该协议在非保密通道下存在两个可能的攻击：保密信息泄露和重放攻击。关键词：电子商务协议；公平性；安全性；形式化分析

3、；ATL中图分类号：TP309文献标识码：A文章编号：1009．5896f2007)04．0901—05Fbrm甜AnalysisofEahE—Co瑚merceProtocolsBasedonATLwenJin分Hua(∞③Lixian矿zhangHuan-guo②LiangMin③zhangMep。u(jh8舌it仳亡eD，—5坳让，nreo凡djrheD7w，G钆i2庇D乱己饥i口e7’sit可，6‰i!／n扎夕550025，(玩inn)吲(&^DDZD，∞唧乱te7’，W包^口佗‰i"er

4、s锄眠^on430072，珊i仃o)吲(』礁，D仃no亡ion如sti亡Ⅱte，G‰i名^D乱j吃凡凸礼ciof』砘s￡i亡“te，G札i∥nr姆550004，CAi佗0)Ab8tr舵t：Aimingatthe8hortcomingthattraditionaltemporallogicsuchasLTL，CTLaIldCTL木reg盯dsprotocol8aselose8yBtemtoanabze，DrKremer(2003)propose8anATL(Alternatin分tiIne11em

5、poralLogic)lo舀c以methodbaLsedongametoanalyzefajrDcommerceprotocols，andanalysesformally8everaltypicalprotocol8ontheirfairnes8andotherproperties．Inthispaper，觚、Llogicalandits印plicationsinformalanalysisof王■commerceprotocolsarediscussed，andDrKremer’approac

6、hisulteriorlyextendedtoanalyzesecurityofprotocol8besides蹦rness．Finally，the8trictformalanalysisismadeforzDBprotocol(1999)proposedbyZhoue亡。己Withthisnewmethod，asaresulttheree)(ists2p08sibleattacksintheZDBprotocolundernon．secrecychannels：leakine88ofsecre

7、tinformationaIldreplyattack8．Keywords：Bcommerceprotocols；Fairness；Security；Fonnalanalysis；ATLl引言电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础，这类协议的基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性等11

8、。与其它密码协议一样，电子商务协议的建模和形式化分析研究非常重要，对于已有成熟的密码协议分析和验证技术可以直接应用到电子商务协议中去。目前

9、在各种电子商务协议形式化分析方法研究中，有影响的方法主要有BAN逻辑方法、Kailar逻辑方法、串空间方法、进程代数方法及基于时序逻辑的方法等【1_引。其中，时序逻辑方法能够通过建立数学模型来描述协议系统，可提供相应的模型检2005—08．30收到，2006—01—11改回国家自然科学基金(40261009)和贵州省科学技术基金(20052111)资助课题测工具对协议性质进行自动验证，对状态空间有限的并发协议系统分析尤为成功，己成为对电子商务协议进行形式化分析的主要工具之一。基于时序逻辑I¨，4