网络安全协议形式化分析技术研究

网络安全协议形式化分析技术研究作者：王芷玲学位授予单位：西安电子科技大学参考文献(59条)1.王育民.刘建伟通信网的安全--理论与技术19992.RNeedham.MSchroederUsingencryptionforauthenticationinlargenetworksofcomputers1978(12)3.范红.冯登国安全协议理论与方法20034.MBurrows.MAbadi.RMNeedhamAlogicofauthentication19895.LiGong.RogerNeedham.RaphaelYahalomReasomingAboutBeliefinCryptographicProtocols19906.MartiNAbadi.MarkRTuttleASemanticsforaLogicofAuthentication(ExtendedAbstract)19917.PvanOorschotExtendingcryptographiclogicsofcryptographiclogicsofbelieftokeyagreementprotocols19938.WenboMao.ColinBoydTowardstheFormalAnalysisofSecurityProtocols19939.PaulSyverson.PaulCvanOorshotOnUnifyingsomeCryptographicProtocolLogics199410.GavinLoweBreakingandFixingtheNeedham-SchroederPublic-KeyProtocolusingFDR199611.SteveSchneiderSecurityPropertiesandCSP199612.GavinLoweTowardsaCompletenessResultforModelCheckingofSecurityProtocols(ExtendedAbstract)199813.AWRoscoe.MHGoldsmithTheperfectSpyforModel-CheckingCryptoprotocols199714.AbadiM.GordonADAcalculusforcryptographicprotocols:Thespicalculus199715.JCMitchell.MMitchell.USternAutomatedAnalysisofCryptographicProtocolsusingMurphi199716.DBolignanoAnapproachtotheformalverificationofcryptographicprotocols199617.LPaulsonProvingpropertiesofsecurityprotocolsbyinduction199718.FJTFabrega.JCHerzog.JDGuttmanHonestidealsonstrandspaces199819.FJTFabrega.JCHerzog.JDGuttmanStrandSpaces:Whyisasecurityprotocolcorrect?199820.MeadowsCUsingtheNRLProtocolAnalyzertoexamineProtocolSuites199821.Yu-QingZHANG.Ji-HongLI.Guo-ZhenXIAOAnapproachtotheformalverificationofthetwo-partycryptographicprotocols1999(04)22.莫燕网络安全协议模型检测技术研究与应用[学位论文]硕士200523.ZhangYuqing.LiuXiuying.YangBoAnapproachtotheformalverificationofthethree-principalcryptographicprotocols2004(01)24.张玉清.王磊.肖国镇.吴建平Needham-Schroeder公钥协议的模型检测分析[期刊论文]-软件学报2000(10)25.IBDamgardPracticalandprovablysecurereleaseofasecretandexchangeofsignatures1995(04)26.SEvenArandomizedprotocolforsigningcontracts1985(06)27.OGoldreichAsimpleprotocolforsigningcontracts198428.MichaelORabinTransactionProtectionbyBeacons1983(02)29.Ben-OrM.GoldreichO.MicaliS.Rivest,RAFairProtocolforSigningContracts199030.AsokanVShoup.MWaidner.VShoup.M.WaidnerOptimisticProtocolsforFairExchange199731.SMicaliSimpleandfastoptimisticprotocolsforfairelectronicexchange200332.AsokanVShoup.MWaidnerOptimisticFairExchangeofDigitalSignatures2000(04)33.RKemmererThreesystemsforcryptographicprotocolAnalysis1994(02)34.AWRoscoeModelingandverifyingkey-exchangeprotocolsusingCSPandFDR199535.CMeadowsTheNRLProtocolAnalyzer:Anoverview1996(02)36.VShmatikov.JMitchellAnalysisofafairexchangeprotocol200037.HPagnia.CGartnerOnTheImpossibilityofFairExchangewithoutaTrustedThirdParty199938.CMeadowsOpenissuesinformalmethodsforcryptographicprotocolanalysis200039.CMeadows.PSyversonAformalspeci-cationofrequirementsforpaymenttransactionsintheSETprotocol40.VKessler.HNeumannAsoundlogicforanalysingelectroniccommerceprotocols41.GiampaoloBella.FabioMassacci.LawrenceCPaulsonPieroTramontano:FormalVerificationofCardholderRegistrationinSET200042.LuS.SmolkaSModelCheckingtheSecureElectronicTransaction(SET)Protocol199943.MPanti.LSpalazzi.STacconiAutomaticverificationofsecurityinpaymentprotocolsforelectroniccommerce,EnterpriseinformationsystemsⅣ200344.MastercardVISASETSecureElectronicTransactionSpecification:Programmer'sGuide199745.MastercardVISASETSecureElectronicTransactionSpecification:BusinessDescription199746.MastercardVISASETSecureElectronicTransactionSpecification:FormalProtocolDefinition199747.GBella.FMassaci.LCPaulsonTheverificationofanindustrialpaymentprotocol:TheSETpurchasephase200248.MFritscher.OKumpSecurityAndProductivityImprovements-SufficientForTheSuccessOfSecureElectronicTransaction200049.SLu.SASmolkaModelCheckingtheSecureElectronicTransaction(SET)Protocol199950.BaoFeng.GuilinWang.JianyingZhouAnalysisandImprovementofMicali'sFairContractSigningProtocol200451.JosepLluísFerrer-Gomila.MagdalenaPayerasoCapellà.LlorencHuguetiRotgeAnEfficientProtocolforCertifiedElectronicMailLectureNotesinComputerScience1975200052.JRMMonteiro.RDahabAnattackonaprotocolforcertifieddelivery200253.GuilinWang.FengBao.JianyingZhouOntheSecurityofaCertifiedE-MailScheme54.MAbadi.RNeedhamPrudentengineeringpracticeforcryptographicprotocols199455.RAnderson.RNeedhamRobustnessprinciplesforpublickeyprotocols199556.PSyversonLimitationsonDesignPrinciplesforPublicKeyProtocols199657.SGritzalis.DSpinellis.PGeorgiadisSecurityProtocolsoveropennetworksanddistributedsystems:Formalmethodsfortheiranalysis,design,andverification1999(08)58.RCanetti.CMeadows.PSyversonEnvironmentalRequirementsforAuthenticationProtocols200259.MOYan.ZHANGYu-Qing.LIXue-GanResearchontheDesignPrinciplesofSecurityProtocol相似文献(10条)1.会议论文孙守卿.李廉.章超.李彩虹基于模型检测工具SPIN的安全协议形式化分析SPIN是一个模拟有限状态并发系统的模型检测工具.本文详细介绍了SPIN的工作原理,并基于SPIN模型检测工具给出了一个简单的安全协议的形式化描述和分析.2.学位论文吴立军时态认知逻辑的模型检测与安全协议验证2005本文主要针对时态认知逻辑的模型检测问题进行了初步研究，研究成果体现在如下几方面：(1)论文首先对安全协议验证的形式化方法进行了概括和总结。并讨论了今后安全协议验证的一些研究方向。安全协议验证的形式化方法主要包括模型检测、定理证明、petri网方法、pi演算方法、csp(CommunicatingSequentialProcesses)方法和串空间方法等。从基本原理、方法及工具到在安全协议验证的应用等方面比较详细的讨论了计算机专家们在形式化方法方面