安全协议形式化验证技术的研究与实现作者:李梦君学位授予单位:国防科学技术大学研究生院参考文献(151条)1.查看详情20042.DDolev.ACYaoOnthesecurityofpublic-keyprotocols1983(29)3.PSyverson.CMeadows.ICervesatoDolev-YaoisnobetterthanMachiavelli20004.RMilnerAcalculusofcommunicationsystems,LNCS925.RMilner.JParrow.DWalkerAcalculusofmobileprocesses,PartⅠandⅡ1992(09)6.Sangiorgi.DWalkerTheπcalculus:aTheoryofMobileProcesses20017.MAbadi.ADGordonAcalculusforcryptographicprotocols:Thespicalculus19978.BBlanchetFromSecrecytoAuthenticityinSecurityProtocols20029.MBurrows.MAbadi.RNeedhamALogicofAuthentication198910.VDGligor.RKailar.SStubblebine.L.GongLogicsforcryptographicprotocols-virtuesandlimitations199111.CBoyd.WMaoOnalimitationofBANlogic199312.LGong.RNeedham.RYahalomReasoningaboutbeliefincryptographicprotocols199013.RajashekarKailarAccountabilityinelectroniccommerceprotocols1996(05)14.PSyversonFormalSemanticsforLogicsofCryptographicProtocols199015.PaulSyversonAddingTimetoaLogicofAuthentication199316.PSyverson.CMeadowsALogicalLanguageforSpecifyingCryptographicProtocolRequirements199317.PSyverson.PVANOorschotOnunifyingsomecryptographicprotocollogics199418.PSyversonKnowledge,beliefandsemanticsintheanalysisofcryptographicprotocols1992(13)19.PaulSyversonATaxonomyofReplayAttacks199420.EClarke.OGrumbergm.DPeledModelChecking199921.SSchneiderSecuritypropertiesandCSP199622.SSchneider.ASpirodopoulosCSPandanonymity199623.GLoweAnAttackontheNeedham-SchroederPublicKeyAuthenticationProtocol199524.GLoweBreakingandfixingtheNeedham-Schroederpublic-keyprotocolusingFDR199625.PeterRyan.SteveSchneiderModellingandAnalysisofSecurityProtocols200126.AWRoscoeModel-checkingCSP199427.AWRoscoeModellingandverifyingkey-exchangeprotocolsusingCSPandFDR199528.MBorealeSymbolictraceanalysisofcryptographicprotocols200129.JCMitchell.MMitchell.USternAutomatedanalysisofcryptographicprotocolsusingmurΦ199730.WMarreroAmodelcheckerforauthenticationprotocols199731.EClarke.SJha.WMarreroUsingstatespaceexplorationandanaturaldeductionstylemessagederivationenginetoverifysecurityprotocols199832.GLoweTowardsacompletenessresultsformodelcheckingsecurityprotocols1999(2-3)33.JCMitchell.VShmatikov.USternFinite-stateanalysisofSSL3.0199834.ZDang.RAKemmererUsingtheASTRALmodelcheckerforcruyptographicaprotocolanalysis199735.VitalyShmatikov.JohnMitchellFinite-stateanalysisoftwocontractsigningprotocols2002(02)36.MFiore.MAbadiComputingSymbolicModelsforVerifyingCryptographicProtocols200137.AHuimaEfficientinfinite-stateanalysisofsecurityprotocols199938.EClark.SJha.WMarreroPartialorderreductionsforsecurityprotocolverification200039.LCPaulsonProvingPropertiesofSecurityProtocolsbyInduction199740.LCPaulsonTheInductiveApproachtoVerifyingCryptographicProtocols1998(01)41.LCPaulsonInductiveanalysisoftheInternetprotocolTLS1999(03)42.LCPaulsonProvingSecurityProtocolsCorrect199943.GBella.FMassacci.LCPaulson.P.TramontanoFormalverificationofcardholderregistrationinSET200044.GBella.LCPaulsonKerberosversioniv:inductiveanalysisofthesecrecygoal199845.FThayerFabrega.JHerzog.JGuttmanStrandspaces:Whyisasecurityprotocolcorrect?199846.FJavier.TFabrega.JCHerzog.JDGuttmanStrandSpace:ProvingSecurityProtocolsCorrect1999(07)47.FThayerFabrega.JHerzog.JGuttmanMixedstrandspaces199948.DXSongAthena:aNewEfficientAutomaticCheckerforSecurityProtocolAnalysis199949.DSong.SBerezin.APerrigAthena:anovelapproachtoefficientautomaticsecurityprotocolanalysis2001(01)50.MAbadi.BBlanchetAnalyzingsecurityprotocolswithsecrecytypesandlogicprograms200251.BBlanchetAnEfficientcryptographicprotocolverifierbasedonprologrules200152.BBlanchetAbstractingCryptographicprotocolsbyPrologRules(invitedtalk)200153.PCousot查看详情200154.CWeidenbachTowardsanAutomaticAnalysisofSecurityProtocolsinFirst-OrderLogic199955.ECohenTAPS:afirst-oderverifierforcryptographicprotocols200056.CMeadowsUsingnarrowingintheanalysisofkeymanagementprotocols198957.CMeadowsRepresentingPartialKnowledgeinanAlgebraicSecurityModel199058.CMeadowsASystemforthespecificationandAnalysisofKeyManagementProtocols199159.CMeadowsApplyingFormalMethodstotheAnalysisofaKeyManagementProtocol1992(01)60.CMeadowsAModelofComputationfortheNRLProtocolAnalyzer199461.CMeadowsFormalverificationofcryptographicprotocols:asurvey199562.CMeadowsTheNRLprotocolanalyzer:anoverview1996(02)63.CMeadowsAnalysisoftheInternetKeyExchangeprotocolusingtheNRLProtocolAnalyzer199964.CMeadowsAformalfiameworkandevaluationmethodfornetworkdenialofservice199965.CMeadowsOpenissuesinformalmethodsforcryptographicprotocolanalysis200066.DBolignanoTowardstheformalverificationofelectroniccommerceprotocols199767.DBolignanoTowardsthemechanizationofcryptographicprotocolverification199768.DBolignanoIntegratingproof-basedandmodel-checkingtechniquesfortheformalverificationofcryptographicprotocols199869.ICervesato.NDurgin.PDLincoln.J.C.MitchellA.ScedrovRelatingstrandsandmultisetrewritingforsecurityprotocolanalysis200070.FButler.ICervesato.AJaggard.A.ScedrovAformalanalysisofsomepropertiesofKerberosVusingMSR200271.ADGordon.AJeffreyAuthenticitybytypingforsecurityprotocols200172.MAbadiSecrecybytypinginsecu