SET协议形式化研究及模型检测摘要：随着移动网络技术的快速发展，电子商务的大量普及，电子商务不在单单只是局限于有线网络，商家们开始将商机延续到移动网络。移动网络用户群体中手机移动上网用户占绝大部分，在这样的商机驱动下，移动电子商务得到快速发展。移动电子商务中最为核心的技术是移动电子支付协议SET,它直接决定了移动电子商务的安全性、高效性。本文就在这样的背景下采用AVISPA工具研究SET协议，通过形式化分析与模型检测，发现了SET协议的支付密钥的不安全性，并给出了攻击路径。关键词：SET协议；模型检测；形式化分析中图分类号：TP309文献标识码：ADoi：10.3969/j.issn.1003-6970.2012.06.039FormalAnalysisandModelCheckingofSETProtocolHUaNGjia(Guizhoutrafficprofessionaltechnologycollege,Guiyang550008)[Abstract]withtherapiddevelopmentofmobilenetworktechnologyandalotofpopularityofelectronicbusiness,e-commerceisnotjustlimitedtocablenetwork.thebusinesseswillcontinuetodevelopmobilenetwork.PhonemobileInternetusershavethemostgroupinmobilenetworkusersmobile,insuchdriveofbusinessopportunities,mobileelectronicbusinessgetfastdevelopment.themostcoretechnologyofmobileelectronicbusinessisthemobileelectronicpaymentprotocolSet,whichdirectlydeterminethesecurityandhighefficiencyofmobilee-business.InthispaperIusetheAVISPAtooltoresearchSETprotocolunderthisbackground,IfoundthesecurityholesofSetprotocolandgivetheattackpathwithformalanalysisandmodelchecking.［Keywords］SETprotocol；Modelchecking；Formalanalysis协议是为了带来交互的安全，但协议被设计出来后并不知是否具有安全性。人们为了从理论的角度分析协议是否具有安全性，研究出协议的形式化分析方法［1］。形式化分析方法包括形式逻辑方法、模型检测方法、定理证明方法。本文主要采用模型检测的方法来研究SET协议的安全性。1模型检测模型检测［2］是一种用于有限状态并发系统自动验证技术。模型检测，狭义的解释为可以看成是决策程序，如果Kripke结构是一个模态逻辑公式，那么能被检测。模型检验,广义的解释为是一个系统验证算法，是在一个系统模型上操作（语义），而不是一个系统描述（语法）O模型检测的优点为不需要证明、检测速度快、给出反例、局部规约可以进行检测、许多并发特性中，逻辑能很容易表达。2AVISPA检测工具AVISPA工具提供了一套建立和分析协议安全的应用软件。协议用高级协议说明语言HLPSL来建模，以描述协议和协议的安全性质。AVISPA工具的结构：一个HLPSL的说明书用转换器hlpsl2if被转换成中间层IFoIF是一个比HLPSL低级的语言，可以被AVISPA工具的后台直接使用。注意，转换的这一步对用户透明，所以是自动的。协议IF说明书被输入AVISPA的后台，分析是否满足安全的目标。AVISPA工具有四个后台：OFMC,CL-AtSe,SATMC和TA4SP；IF就是被设计来方便这些后台分析这些输入的语言。而且，这些分析方法是部分互补的而不是等价的，所以，不同的分析方法可能产生不同的分析结果。本协议的检测主要采用后台0FMC,下面对其进行详细概述。On-the-Fly模型检测器OFMC[3]是在需要驱动的协议分析方法上，建立一个无限树。它用了一些符号表示法来表示状态空间。正是在这样的技术下，OFMC在没有给出具体入侵者能产生的消息的情况下，而高效的检测协议的伪造，和一些会话过程的验证。在现在的版本中，OFMC最显著的特性是用户可以说明在消息项上说明一个代数的理论，来建模协议分析的运行。OFMC还将符号表示法和惰性入侵技术相结合，其运行也需要驱动。{DualSig^・PF}_Kr・{AI・K1‘}_EncK_P)/\witness(C,M,deal,01'・h(PI，))/\witness(C,P,deal,01'・PI‘)/\secret(OrderDesc,order,{C,M})/\secret(PurchAmt,order,{C,M,P})/\secret(PI',payment,{C,P})3.S二2/\RCV(LIDM.XID.ChallC.h(PurchAmt).{h(LIDM.XID.Chai1C.h(PurchAmt))}inv(SignKM))二>S'：=3/\request(C,M,deal,01.h(PI))endrole使用AVISPA检测工具的OFMC后台对SET协议进行检测,检测结果如下：...