基于进程演算的安全协议形式化研究

FormalResearchofSecurityProtocolsBasedOnProcessCalculus200512(1)SpiSpiKerberos(2)AppliedpiiKPSpiAppliedpi3FORMALRESEARCHOFSECURITYPROTOCOLSBASEDONPROCESSCALCULUSABSTRACTWiththewideapplicationandrapiddevelopmentcomputernet-workisgraduallyacceptedbymanykeydepartments,whichleadstovariousandcomplexrequirementsofsecurity.However,manyexistingsecurityprotocolsareprovennottobesoreliableaswhatwereexpected.Meanwhile,thenetworksystemsstillfaceuptovariousthreatsofneworoldattackingmethods.Thecomplicationofnetworkenvironmentmakestheattackerpossibletolaunchvariousattacksfromthe°awsintheprotocolstobreaknetworksecurity.Sosecurityprotocolsarecrucialtonetworksecurity.Formalmethodsforprotocolanalysiscanmakethedesignerfocuson,throughsystemanalysis,interfaces,hypothesesoftheenvironment,systemstatesundervariousconditions,exceptionswhensomeconditionsarenotsatis¯edandinvariantproperties.Formalmethodscanalsopro-vide,throughsystemvalidation,guaranteesofsecuritiesofprotocols.Recently,formalmethodsforprotocolanalysisaremainlyofthreekinds:methodsbasedonmodallogicofknowledgeandbelief,methodsbasedontheoremproofandmethodsbasedonprocesscalculus.Amongthemthree,sinceprocesscalculusdescriptionsapproachthenatureofproto-cols,itcandepicttherunningprocessofprotocolsprecisely.Whenusing4processcalculusforprotocolanalysisandvalidation,eachprincipalismodelledasasingleprocess,alltheseprocessesrunconcurrentlyandcommunicateinasynchronizedmannerthroughsharedchannels,andtheresultingconcurrentsystemisregardedasthemodeloftheprotocol.Processcalculusmethodscanutilizebothbasictheoremsandmethodsfromalgebramodellingandmethodsfromabstractprogramminglan-guageanalysis.So,methodsbasedonprocesscalculuscanbedividedintothreeaspects:modelchecking,validationthroughbisimulationandprogramanalysis.Thereexistsomeresearchresultsbasedonprocesscalculusinthisdissertation,solvingsomeproblemsneverbesolvedbefore.Researchforegroundshavealsobeenconcludedandprospected.Themaincontentsandcontributionsareasfollows:(1)AprimitivehasbeenextendedinSpicalculussothatitcanverifysecurityprotocolswithtimestamp.Andbasedonthisextendedcalculus,theauthenticationofKerberosprotocolhasbeenveri¯ed.(2)Tillnow,Therearenootherformalresearchofsecurityprotocolsfocusonanonymityproperty.Inthisdissertation,WhetheriKPprotocolhasanonymitypropertyisdiscussedbasedonappliedpicalculus.Anditsauthenticationisalsobeenveri¯edatthesametime.KEYWORDS:securityprotocols,processcalculus,Spicalculus,Appliedpicalculusauthenication,anonymity5111.1............................................................................11.2......................................................21.3.........................................................41.3.1..................................41.3.2......................................................61.4.....................................71.4.1...................................................................71.4.2..................................101.4.3.............................111.5..............................................................151.6............................................................................162Spi172.1..................................................................................172.2Spi.............................................................172.2.1Spi.............................................................172.2.2Spi.............................................................182.3............................................................................212.3.1...................................................................212.3.2Framed.......................................................222.4Spi.......................................................242.4.1Kerberos.............................................................242.4.2Kerberos................................................262.4.3Kerberos..............................................272.4.4Kerberos......................................................282.4.5Kerberos...........................................282.5....................................................................2963Appliedpi303.1..................................................................................303.2.........................................................................313.2.1Appliedpi....................................................313.2.2Appliedpi....................................................323.3............................................................................343.3.1...................................................................343.3.2...................................................................353.4Appliedpi..............................................353.4.1ikp....................................................................353.4.21kp.......................................................383.4.31kp....................................................403.4.41kp....................................................403.5....................................