安全协议形式化分析理论与方法研究综述

安全协议形式化分析理论与方法研究综述作者：冯登国，范红作者单位：中国科学院软件研究所,北京,100080刊名：中国科学院研究生院学报英文刊名：JOURNALOFTHEGRADUATESCHOOLOFTHECHINESEACADEMYOFSCIENCES年，卷(期)：2003，20(4)引用次数：19次参考文献(66条)1.RMNeedham.MDSchroederUsingEncryptionforAuthenticationofLargeNetworksofComputers1978(12)2.DDenning.GSaccoTimestampsinKeyDistributionProtocols1981(8)3.DDolev.AYaoOntheSecurityofPublicKeyProtocols1983(2)4.MBurrows.MAbadi.RNeedhamALogicofAuthentication19895.PartsandVersionsofthisMaterialHaveBeenPresentedinManyPlacesIncluding:ACMTransactionsonComputerSystems,1989,8(1):18～3619896.PaulSyversonATaxonomyofRelayAttacks19947.LGong.RNeedham.RYahalomReasoningaboutBeliefinCryptographicProtocols19908.MAbadi.MRTuttleASemanticsforaLogicofAuthentication19919.PFSyverson.PCvanOorschotOnUnifiedSomeCryptographicProtocolLogics199410.RKailarAccountabilityinElectronicCommerceProtocols1996(5)11.DKindredTheoryGenerationforSecurityProtocols:[Ph.DThesis]199912.MichaelBurrows.MartinAbadi.RogerNeedhamAuthentication:APracticalStudyinBeliefandAction198813.MichaelBurrows.MartinAbadi.RogerNeedhamALogicofAuthentication1990(1)14.PFSyverson.PCvanOorschotAUnifiedCryptographicProtocolLogic199615.RonaldL.RivestAdiShamir.DavidAWagner:Timed-lockpuzzlesandTimed-ReleaseCryptographicprotocol199616.TCoffey.PSaidhaLogicforVerifyingPublic-keyCryptographicProtocols1997(1)17.GLoweBreakingandfixingtheNeedham-Schroderpublic-keyprotocolusingFDR199618.JBums.CJMitchellASecuritySchemeforResourceSharingOveraNetwork199019.CMeadowsAModelofComputationfortheNRLProtocolAnalyzer199420.ThomasYCWoo.SimonSLam:AuthentificationforDistributedSystems1992(1)21.TGenet.FKlayRewritingforCryptographicProtocolVerification200022.TGenet.FKlayRewritingforCryptographicProtocolVerification(extendedversion).TechnicalReport.CNET-FranceTelecom199923.RichardAKemmererAnalyzingEncryptionProtocolsUsingFormalVerificationTechniques1989(4)24.JScheid.SHoltsbergInaJoSpecificationLanguageReferenceManualSystemsDevelopmentCroup.UnisysCorporation,1988.MichaelBurrows,MartinAbadi,RogerNeedham1990(1)25.CARHoareCommunicatingSequentialProcesses198526.WillMarrero.EdmundClarke.SomeshJhaAModelCheckerforAuthenticationProtocols199727.GLoweBreakingandFixingtheNeedham-SchroderPublic-KeyProtocolUsingFDR199628.TYCWoo.SSLamASemanticModelforAuthenticationProtocols199329.DLongley.SRigbyUseofExpertSystemsintheAnalysisofKeyManagementSystems198930.JonathanKMillen.SidneyCClark.SherylBFreedmanTheInterrogator:ProtocolSecurityAnalysis1987(2)31.PaulSyverson.CatherineMeadowsALogicalLanguageforSpecifyingCryptographicProtocolRequirements199332.GustavusJSimmonsHowto(Selectively)BroadcastaSecret198533.DLongley.S.RigbyAnAutomaticSearchforSecurityFlawsinKeyManagementSchemes1992(1)34.BolignanoDAnApproachtotheFormalVerificationofCryptographicProtocols199635.LCPaulsonProvingPropertiesofSecurityProtocolsbyInduction199736.SSchneiderUsingCSPforProtocolAnalysis:theNeedham-SchroederPublicKeyProtocol199637.FJavierThayerFabrega.JonathanCHerzog.JoshuaDGuttmanHonestIdealsonStrandSpaces199838.FJavierThayerFabrega.JonathanCHerzog.JoshuaDGuttmanStrandSpacesPictures199839.FJavierThayerFabrega.JonathanCHerzog.JoshuaDGuttmanStrandSpace:WhyIsaSecurityProtocolCorrect?199840.AWRoscoeModelingandVerifyingKeyExchangeProtocolsUsingCSPandFDR199541.GavinLowe.BillRoscoeUsingCSPtoDetectErrorsintheTMNProtocol1997(10)42.NHeintze.JDTygarAModelforSecureProtocolsandTheirComposition1996(16)43.ScottDStollerABoundonAttacksonPaymentProtocols200144.MeadowsCUsingtheNRLProtocolAnalyzertoExamineProtocolSuites199845.LCPaulsonTheInductiveApproachtoVerifyingCryptographicProtocols199846.AlecYasinsacAFormalSemanticsforEvaluatingCryptngraphicProtocols199647.SBrackinAnInterfaceSpecificationLanguageforAutomaticallyAnalyzingCryptographicProtocols199748.JMillenCAPSL:CommonAuthenticationProtocolSpecificationLanguage199749.JMillenCAPSLSemantics199750.JMillenTermReplacementAlgebrafortheInterrogator199751.JMillenTheInterrogatorUser＇sGuide199752.GLoweAHierarchyofAuthenticationSpecifications199753.GAghaAbstractingInteractionPatterns:AProgrammingParadigmforOpenDistributeSystems199754.SBrackinEvaluatingandImprovingProtocolAnalysisbyAutomaticProof199855.SecureElectronicTransaction(SET)specification199656.RMilner.JParrow.DWalkerACalculusofMobileProcesses,PartsⅠandⅡ199257.JGray.JMcleanUsingTemporalLogictoSpecifyandVerifyCryptographicProtocols(ProgressReport)199558.LGong.PSyversonFail-StopProtocols:AnApproachtoDesigningSecureProtocols199559.MAbadi.RNeedhamPrudentEngineeringPracticeforCryptographicProtocols1996(1)60.BrackingSAState-BasedHOLTheoryofProtocolFailure61.SBrackinDecidingCryptographicProtocolAdequacywithHOL:TheImplementation199662.题词[期刊论文]-网络安全技术与应用2001(1)63.冯登国国内外密码学研究现状及发展趋势[期刊论文]-通信学报2002(5)64.StefanosGritzalis.DiomidisSpinellisTheCascadeVulnerabilityProblem:TheDetectionProblemandaSimulatedAnnealingApproachforitsCorrection1998(10)65.FJavierThayerFabrega.JonathanCHerzog.JoshuaDGuttmanStrandSpace:WhyisaSecurityProtocolCorrect?199866.SBELLOVIN.MMerrittEncryptedKeyExchange:Password-BasedProtocolsSecureAgainstDictionaryAttacks1992相