电子商务安全协议的形式化分析技术研究

西安电子科技大学硕士学位论文电子商务安全协议的形式化分析技术研究姓名：吴建耀申请学位级别：硕士专业：密码学指导教师：杨波20050101电子商务安全协议的形式化分析技术研究作者：吴建耀学位授予单位：西安电子科技大学参考文献(51条)1.参考文献2.王育民.刘建伟通信网的安全--理论与技术19993.RNeedham.MSchroederUsingencryptionforauthenticationinlargenetworksofcomputers1978(12)4.ClarkJ.JacobJAsurveyofauthenticationprotocolliterature:Version1.019975.ISO.IECInformationtechnologysecuritytechniquesentityauthenticationmechanismspart2:Entityauthenticationusingsymmetrictechniques19936.SatyanarayananMIntegratingsecurityinalargedistributedsystem19877.ISO.IECInformationtechnologysecuritytechniquesentityauthenticationmechanismspart4:Entityauthenticationusingcryptographiccheckfunctions19938.OtwayD.ReesOEfficientandtimelymutualauthentication1987(01)9.BurrowsM.AbadiM.NeedhamRAlogicofauthentication198910.DenningD.SaccoGTimestampsinkeydistributionprotocols1981(08)11.WooT.LamSAlessononauthenticationprotocoldesign1994(03)12.NeumanBC.StubblebineSGAnoteontheuseoftimestampsasnonces1993(02)13.KaoIL.ChowRAnefficientandsecureauthenticationprotocolusinguncertifiedkeys1995(03)14.ISO.IECInformationtechnologysecuritytechniquesentityauthenticationmechanismspart3:Entityauthenticationusingapublickeyalgorithm199515.DiffieW.HellmanMENewdirectionsincryptography1976(06)16.RNeedham.MSchroederUsingencryptionforauthenticationinlargenetworksofcomputers1978(12)17.NetscapeSecureSockerLayer200218.MasterCard&VISASETSecureElectronicTransactionSpecification:Programmer'sGuide199719.MasterCard&VISASETSecureElectronicTransactionSpecification:BusinessDescription199720.MasterCard&VISASETSecureElectronicTransactionSpecification:FormalProtocolDefinition199721.SihanQingNotesonLogicAnalysisofCryptographicProtocols22.CBoyd.WMaoLimitationsofLogicalAnalysisofCryptographicProtocols23.LiGong.RogerNeedham.RaphaelYahalomReasomingAboutBeliefinCryptographicProtocols199024.MartiNAbadi.MarkRTuttleASemanticsforaLogicofAuthentication(ExtendedAbstract)199125.vanOorschotExtendingcryptographiclogicsofcryptographiclogicsofbelieftokeyagreementprotocols199326.WenboMao.ColinBoydTowardstheFormalAnalysisofSecurityProtocols199327.PaulSyverson.PaulCvanOorshotOnUnifyingsomeCryptographicProtocolLogics199428.RKailarAccountabilityinElectronicCommerceProtocols1996(05)29.GavinLoweBreakingandFixingtheNeedham-SchroederPublic-KeyProtocolusingFDR199630.SteveSchneiderSecurityPropertiesandCSP199631.GavinLoweTowardsaCompletenessResultforModelCheckingofSecurityProtocols(ExtendedAbstract)199832.AWRoscoe.MHGoldsmithTheperfectSpyforModel-CheckingCryptoprotocols199733.AbadiM.GordonADAcalculusforcryptographicprotocols:Thespicalculus199734.JCMitchell.MMitchell.UStemAutomatedAnalysisofCryptographicProtocolsusingMurphi199735.FJTFabrega.JCHerzog.JDGuttmanHonestidealsonstrandspaces199836.FJTFabrega.JCHerzog.JDGuttmanStrandSpaces:Whyisasecurityprotocolcorrect?199837.Yu-QingZHANG.Ji-HongLI.Guo-ZhenXIAOAnapproachtotheformalverificationofthetwo-partycryptographicprotocols1999(04)38.SMV39.MTatebayashi.NMatsuzaki.DBNewmanKeydistributionprotocolfordigitalmobilecommunicationsystems198940.MillerSP.NeumanC.SchillerJI.SaltzerJHKerberosauthenticationandauthorizationsystem.ProjectAthenaTechnicalPlanSectionE.2.1198741.张玉清.王磊.肖国镇.吴建平Needham-Schroeder公钥协议的模型检测分析[期刊论文]-软件学报2000(10)42.刘秀英.张玉清.杨波.邢戈三方密码协议运行模式分析法[期刊论文]-中国科学院研究生院学报2004(3)43.LuS.SmolkaSModelCheckingtheSecureElectronicTransaction(SET)Protocol199944.GBella.FMassaci.LCPaulsonTheverificationofanindustrialpaymentprotocol:TheSETpurchasephase200245.MFritscher.OKumpSecurityAndProductivityImprovementsSufficientForTheSuccessOfSecureElectronicTransaction200046.MPanti.LSpalazzi.STacconiAutomaticverificationofsecurityinpaymentprotocolsforelectroniccommerce200347.MAbadi.RNeedhamPrudentengineeringpracticeforcryptographicprotocols.[ResearchReport125,DigitalEquipmentCorporationSystemsResearchCenter]199448.RAnderson.RNeedhamRobustnessprinciplesforpublickeyprotocols199549.PSyverson查看详情199650.SGritzalis.DSpinellis.PGeorgiadisSecurityProtocolsoveropennetworksanddistributedsystems:Formalmethodsfortheiranalysis,design,andverification1999(08)51.SGritzalis.DSpinellisCryptographicProtocolsoverOpenDistributedSystems:ATaxonomyofFlawsandrelatedProtocolAnalysisTools1999相似文献(1条)1.学位论文任桃基于SSL协议的访问控制机制研究与实现2008随着网络技术的飞速发展，网络应用已经渗透到我们生活的方方面面，但网络给人们带来巨大便利的同时也带来了一些潜伏的不安全因素。网络的发展带动了电子商务的广泛应用，它的安全性问题逐步得到了人们的重视。SSL安全套接层协议是基于C/S结构的保护应用层数据的协议，已经在网络环境中得到了广泛的应用，是一种优秀的安全协议。它作为一种广泛应用的电子商务安全协议，通过在握手协议中使用密钥协商来加密通信数据。尽管SSL已经有十多年的历史，但它仍然在握手部分存在访问控制应用缺陷。针对SSL访问控制应用中的缺陷，传统的基于SSL协议的访问控制机制在权限认证方面都有不足之处。针对这个问题，本文主要的工作有：首先，本文设计了一个基于PMI属性证书的SSL协议。PMI是由PKI发展而来，PKI提供强认证服务，而PMI提供灵活的权限认证。PMI中的属性证书与身份证书相似，把属性、群组、角色信息包含在证书中。在分析属性证书和身份证书的绑定方式的基础上，本文采用了自由绑定方式进行协议的改进设计。该改进协议主要针对握手协议部分，在服务器向客户端请求证书时加入了一个对客户端属性证书的请求。与此同时，服务器验证客户端身份证书后，对属性证书进行验证，验证不通过则无法进行访问。这使服务器信息得到了更好的保护，增强了原SSL协议的安全性。属性证书的管理则交给PMI授权管理基础设施，同时授权管理也更为灵活。其次，本文使用BAN逻辑对该改进协议进行了形式化分析。BAN逻辑是一种最为简单、实用的形式化分析方法，使用它可推导认证的结果，发现大部分的安全漏洞和冗余信息。形式化分析结果表明该改进协议是一个可行的安全解决方案，在并未破坏原SSL协议安全目标的前提下，完成了主体属性信息的交换。最后，本文基于该改进协议构造了一个安全系统，该系统包含两个功能模块：身份鉴别和权限管理。系统使PKI和PMI联合认证，具有较高的安全性。本文链接：