摘要本文主要对逻辑方法与模型检测技术及其在电子商务协议并形式化分析中的应用进行了系统研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术，其工作主要有以下几个方面:1.对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提出电子商务协议设计的基本准则。2.对当前流行的电子商务协议形式化分析方法进行重点研究，包括BAN逻辑、Kailar逻辑及周—卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺陷并提出新的公平非否认性协议。关键词：电子商务协议，形式化分析，逻辑方法，模型检测，博弈逻辑四号、黑体、加粗五号、宋体、1.5倍行间距五号、宋体、用逗号分隔AbstractThedissertationmainlystudiestheapplicationsoflogicandmodelcheckingmethodsinformalanalysisofE-commerceprotocols.Ingeneral,theauthorstudiestherelatedformalanalysistechnologyofE-commerceprotocolsfromtwoaspects,theoryandapplications.Themainworksandresultsareasfollows:1.AnalyzesanddiscussesthebasictheoriesandcharactersofE-commerceprotocols,includes:security,secrecy,integrity,authentication,non-repudiation,fairness,timelinessandetc.redefinesomekeysignificantcharacters,andbringforwardsomenewrulesofE-commerceprotocolsdesign.2.StudiesthecurrentformalanalysismethodsforE-commerceprotocols:BANlogic、KailarlogicandZhou-Qingapproach.Usetheabovemethodstoanalyzingsomeimportantprotocols,findoutitslimitationsandbringforwardanewfairnon-repudiationprotocol.Keywords：E-commerceProtocols,formalanalysis,logicmethod,SymbolicModelChecking,gamelogic四号，TimesNewRoman加粗、居中五号，TimesNewRoman加粗五号，TimesNewRoman，用逗号分隔开目录摘要...................................................................................................................................................IAbstract............................................................................................................................................II1.绪论...............................................................................................................................................11.1课题背景.....................................................................................................................................12.电子商务协议...............................................................................................................................22.1密码协议.....................................................................................................................................27结束语...........................................................................................................................................37.1主要研究工作............................................................................................................................37.2下一步工作................................................................................................................................3参考文献..........................................................................................................................................4致谢................................................................................................................................................5附录1:参考文献基本格式.........................................................................................
