一种分析电子商务协议的新方法

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

1、第27卷第4期计算机学报Voi.27No.42004年4月CHINESEJOURNALOFCOMPUTERSApr.2004一种分析电子商务协议的新方法1）2）王彩芬葛建华1）（西北师范大学数学与信息科学学院兰州730070）2）（西安电子科技大学ISN国家重点实验室西安710071）摘要通过将Kaiiar逻辑和LPC形式方法相结合，提出一种新的用于分析电子商务协议的形式化方法.新方法中的推导规则既简单便捷同时又具有分析签名和分析密文的能力.该方法既能描述协议中参加者的行为又能够分析参加者拥有的知识和推导协议的可追究

2、性和公平性，使用该方法不仅可以分析使用在线第三方的协议又可以分析使用脱线第三方的电子商务协议.与其它的方法相比较，这一新方法既避免了Kaiiar逻辑的缺陷又弥补了LPC方法的不足.关键词电子商务；协议；可追究性；公平性；形式化分析中图法分类号TP309ANewApproachfortheAnalysisofElectronicCommerceProtocols1）2）WANGCai-FenGEJian-Hua1）（CollegeofMathematicsandInformationScience，NorthwestN

3、ormalUniuersity，Lanzhou730071）2）（NationalKeyLaboratoryonISN，XidianUniuersity，Xi'an710071）AbstractThispaperpresentsanapproachfortheanaiysisofe-commerceprotocoisbycombiningKaiiariogicwithLPCorganicaiiy.Thisapproachprovidesasetofinferenceruiesforreductionandanaiys

4、isofsignatureandcryptograph.Thusitnotoniydescribestheknowiedgeandbehaviorofparticipants，butaisoanaiyzestheaccountabiiityandfairnessofe-commerceprotocois.Inaddition，theuseofthemethodena-biesustoanaiyzeprotocoisbothwithin-iineTTPandwithoff-iineTTP.Comparedwithoth

5、erapproach，thisonecanheipavoidtheweaknessofKaiiariogicandcompensatethedeficiencyoftheLPC.Keywordse-commerce；protocois；accountabiiity；fairness；formaianaiysis密码协议一样，经过精心设计的协议往往存在安全1引言上的漏洞，而这些漏洞用非形式的方法是难以发现的.通过形式化的分析方法说明协议正确性成为非电子商务协议是实现电子商务的重要技术基常必要的手段.础.公平性和可追究性

6、是协议中最重要的性质.协议基于逻辑的形式化方法最初用来分析认证密码［1］的公平性保证参加协议的各方在协议执行的任何阶协议，其中最著名的当属BAN逻辑.虽然BAN逻段都处于同等地位，当协议执行完后或者各方得到辑在分析认证等性质时是很有效的，然而，电子商务各自所需的或者什么也得不到；可追究性保证协议协议除了包括认证性质外还包括非否认性和公平性中任何一方在协议执行完后，能够提供充分的证据的内容，也还有其它内容的扩充.因此，对电子商务以解决今后可能遇到的争论.电子商务协议与其它协议的理论分析如BAN及BAN-类的逻辑已无法适

7、收稿日期：2002-11-12；修改稿收到日期：2003-12-24.本课题得到西北师范大学重点研究方向基金资助.王彩芬，女，1963年生，博士，教授，主要研究方向为信息安全、电子商务中协议的安全以及协议的形式化分析.E-maii：wangcaifen@yahoo.com.cn.葛建华，男，1961年生，博士，教授，博士生导师，主要研究方向为网络安全和HDTV.508计算机学报2004年用.Kaiiar在文献［2］中基于BAN逻辑提出分析电通配符或占位符（n？）或一个名字（n）：子商务协议的可追究性逻辑，但该逻辑不能

8、分析电pattern=｛pl，p2，⋯，p｝keykey？key？.子商务协议的公平性，文献［3］中还指出Kaiiar逻定义5.消息-模式匹配操作（~）定义如下（1，辑存在其它主要的缺陷.逻辑的方法只能模型化参1iEVAL，p，piEPAT，key，keyiEKEY，mEMSG，nE与者的消息和信任，不能提供表示和推导参与者行NAM