Internet安全協(xié)議與分析

基于攻擊結(jié)構(gòu)性方法問題VMS的工作機(jī)理是什么？如何以暴力破解形式來分析協(xié)議安全性？本次課程教學(xué)安排CSP基礎(chǔ)基于CSP的安全協(xié)議建?！癉olev-Yao”ModelInspiredbya1983paperD.DolevandA.Yao.“Onthesecurityofpublickeyprotocols”.IEEETransactionsonInformationTheory,29(2):198-208.AdversaryisanondeterministicprocessCanreadanymessage,decomposeitintopartsandre-assembleCannotgainpartialknowledge,performstatisticaltests,…“Dolev-Yao”Model“Black-box”cryptographyAdversarycandecryptifandonlyifheknowsthecorrectkeyAssumesthatcryptographicfunctionshavenospecialpropertiesMostmechanizedformalmethodsforsecurityanalysisusesomeversionofthismodelCSP概念CSP(CommunicatingSequentialProcesses)isanotationfordescribingsystemsofparallelagentsthatcommunicatebypassingmessages.CSP是用于刻畫交互的一種模型CSP常見符號CSP常見符號CSP常見符號CSP常見符號CSP形式化定義Asmallmathematicallanguagecontainingthemainconstructsforspecifyingconcurrency,parallelism,communication,choiceetc.Theevolutionofprocessesisbasedonasequenceofeventsor

actionsVisibleactionsSInteractionwithotherprocesses,communicationInvisibleactiontInternalcomputationstepsCSP語法（Stop&Input）Inaction:StopTermination,

deadlock,incapabilityofperforminganyaction,eitherinternalorexternalInput:in?x:AgP(x)Executeaninputactiononchannelin,getmessagexoftypeA,thencontinueasP(x)CSP語法（Output&Recursion）Output:out!mgP(x)Executeanoutputactiononchannelout,sendmessagem,thencontinueasP(x)Recursion:P(y1,…,yn)=Body(y1,…,yn)Processdefinition.Pisaprocessname,y1,…,ynaretheparameters,Body(y1,…,yn)isaprocessexpressionExample:Copy=in?xgout!mgCopyCSP語法（Externalchoice）Externalchoice:P[]QExecuteachoicebetweenPandQ.Donotchooseaprocesswhichcannotproceed

Example:(a?xgP(x))[]

(b?xgQ(x))

Executeoneandonlyoneinputaction.Ifonlyoneisavailablethenchoosethatone.Ifbothareavailablethanchoosearbitrarily.Ifnoneareavailablethenblock.Theunchoosenbranchisdiscarded(commitment)CSP語法（Internalchoice）Internalchoice:P+QExecuteanarbitrarychoicebetweenPandQ.Itispossibletochooseaprocesswhichcannotproceed

CSP語法（Paralleloperator）Paralleloperatorwithsynchronization:P||QPandQproceed

inparallelandareobligedtosynchronizeonallthecommonactions

Example:(c?xgP(x))||

(c!mgQ)Synchronization:thetwoprocessescanproceedonlyiftheiractionscorrespondHandshaking:sendingandreceivingissymultaneous(clearlyanabstraction.Bufferedcommunicationcananywaybemodeledbyimplementingabufferprocess)CSP語法Communication:mistransmittedtothefirstprocess,whichcontinuesasP(m).Broadcasting:c!misavailableforotherparallel

procsQuestion:whathappenswiththeprocess((c?xgP(x))[](d?ygQ(y)))||(c!mgR)CSP語法（interleaving）Paralleloperatorwithsynchronizationandinterleaving:P||AQPandQareobligedtosynchronizeonlyonthecommonactions

inA

TheyinterleaveonalltheactionsnotinACSP語法（interleaving）Example:

(c?xgP(x))||{c}((c!mgQ)[](d!ngR))thetwoprocessescaneithersynchronizeontheactiononchannelc,orthesecondprocesscanperformanactionond.Inthissecondcasethefirstprocesswillremainblocked,though,untilthesecondwilldecidetoperform(ifever)anoutputactiononc.Question:inwhatpartofthesecondprocesscouldthisactiononcbeperformed?Abbreviation:

P|||QstandsforP||fQPREFIXRECURSIONX=F(X)CHOICETRACEAtraceofthebehaviourofaprocessisafinitesequenceofsymbolsrecordingtheeventsinwhichtheprocesshasengageduptosomemomentintime.Imaginethereisanobserverwithanotebookwhowatchestheprocessandwritesdownthenameofeacheventasitoccurs.InteractionExampleGENERALCHOICEFDRFailuresDivergencesRefinementCheckersSpecificationandImplementationsFDR2--http://www.cs.ox.ac.uk/projects/concurrency-tools/NS公鑰協(xié)議消息刻畫信道定義Channeluser,session,I_running,R_running,I_commit,R_commit:Initiator,Responder.進(jìn)程刻畫含有攻擊的刻畫攻擊者攻擊者系統(tǒng)的進(jìn)程刻畫認(rèn)證的含義對于響應(yīng)者的認(rèn)證，當(dāng)且僅當(dāng)B確實參與到協(xié)議的運(yùn)行中時，A才