密碼協(xié)議書稿中文第9章

4章中提出的新鮮性原則已經(jīng)被用來有效地分析密碼協(xié)議的安全性，這是因?yàn)樾迈r有效性[1-4]7章中，已經(jīng)提出了基于可信任新鮮性的安全性分析的模態(tài)邏輯，即信任本章將給出一個(gè)基于新鮮性原則的協(xié)議安全性邏輯分析工具（4章SPEARII框架中的一些概念[5,6]。SPEARI，全稱是“安全協(xié)議工程和分析資源”[8]J.P.Bekmann，P.GoedeA.Hutchison1997年開發(fā)，目的是幫助密碼協(xié)議的設(shè)計(jì)和安全性分析。SPEARI的兩個(gè)主要目標(biāo)是使協(xié)議設(shè)計(jì)安全高效，并支持協(xié)議源代碼的生成。SPEARI為密碼協(xié)議的開發(fā)者提供用BAN邏輯進(jìn)行協(xié)議的安全性分析[9]。SPEARIIII”[6]SPEARI基礎(chǔ)上的協(xié)議工程工具。SPEARII工具的目的是使密碼協(xié)議工程分析變得更容易，它通過為用戶提供適GNYGNYGNY語句快速、準(zhǔn)確和語法下細(xì)化一個(gè)協(xié)議的消息、初始假設(shè)和安全目標(biāo)。在此之后，GNY規(guī)則集合被引入并在GNY為一個(gè)GYNGER分析者提供友好的用戶界面。SPEAEII提供了基于圖形的協(xié)議分析FDRFailuresDivergencesRefinement)[10–12]CSP[13]基礎(chǔ)上的狀性是否被滿足。1995Lowe使用自動模型檢驗(yàn)工具FDR成功發(fā)現(xiàn)了著名的次被發(fā)現(xiàn)有漏洞[10,11]。在FDR中，協(xié)議中的主體（甚至可能是一個(gè)攻擊者）被看作是并發(fā)CSP進(jìn)程，而攻擊者進(jìn)程可以執(zhí)行多種攻擊操作(竊聽，冒充，重放等等)。協(xié)議的安全性由主體事件的序列來刻劃，而FDR工具則被用來檢驗(yàn)協(xié)議的主體各事件序列是否滿足安全性質(zhì)。CSP的模型檢驗(yàn)工具在分析Needham-Schroeder公鑰認(rèn)證協(xié)議中獲得了成功。NRL協(xié)議分析器[14]MeadowsProlog的模型檢驗(yàn)工具，其中“NRL”是美國海軍研究實(shí)驗(yàn)室的縮寫。NRLDolev-Yao通信威脅模型[15]Dolev-YaoDolev-Yao模型中，攻擊者的計(jì)算能力是多項(xiàng)式有界的，在協(xié)議執(zhí)行之NRL協(xié)議分析器已被用來分析許多認(rèn)證協(xié)議，并且成功發(fā)現(xiàn)或證明其中一些協(xié)議已知Needham-Schroeder公鑰認(rèn)證協(xié)議[16]（MeadowsNRL協(xié)議分析器進(jìn)行的協(xié)議分析和使用文獻(xiàn)[11]FDR的協(xié)議安全性分析進(jìn)行了一個(gè)比較絡(luò)密鑰交換協(xié)議（IKE2”交換協(xié)議的簽名中發(fā)現(xiàn)了反射攻擊）[17,18]和安全Murφ是一種協(xié)議驗(yàn)證工具[20]，它已經(jīng)成功的應(yīng)用在一些工業(yè)協(xié)議上，尤其是在多處理器緩Murφ語言是一種描述有限狀態(tài)異步并發(fā)系統(tǒng)的高級語言，而MurφMurφ程序C++MurφMurφ語言描述出來，然后用所需Murφ中表示，即布爾條件，在每一個(gè)達(dá)到的狀態(tài)中都必須是正確的。Murφ系統(tǒng)將自動檢查模型的所有可達(dá)狀態(tài)是Murφ模型是不確但不是一般協(xié)議的正確性。如果一個(gè)包含一些違規(guī)不變量的狀態(tài)是可達(dá)的，Murφ就能夠給出對這個(gè)錯(cuò)誤的追蹤，一個(gè)從起始狀態(tài)到出現(xiàn)問題狀態(tài)的狀態(tài)序列。Murφ證明了對一些已Needham-Schroeder公鑰協(xié)議，TMNKerberosv5的一個(gè)簡單版本是存在讀寫器JonathanMillen，SidneyClarkSherylFreedman1985Prolog能的攻擊中如何能夠獲得數(shù)據(jù)項(xiàng)。讀寫器和它的相關(guān)的圖形界面用LM-Prolog在一個(gè)是用來在多種應(yīng)用領(lǐng)域生成特殊證明目標(biāo)的通用證明工具。SyMP的核心工具是一個(gè)連接著值得注意的是，SyMP證明器并沒有內(nèi)置的模型檢驗(yàn)器。SyMP有兩套證明系統(tǒng)：默認(rèn)的證明系統(tǒng)和Athena。默認(rèn)的證明系統(tǒng)實(shí)現(xiàn)了一個(gè)廣義的Athena證明系統(tǒng)用于密碼協(xié)議的安全性驗(yàn)證，利用串空間[26]作為協(xié)議表示的基礎(chǔ)，基DSongAthena[27]技術(shù)構(gòu)建框架。Athena程序的文件后綴名是“.ath”?？蚣苤械腃APSL(CommonAuthenticationProtocolSpecificationLanguage)，即通用認(rèn)證協(xié)議描述語CAPSL中使用分析者提供。CAPSL環(huán)境包括了對這類信息的詳細(xì)描述。環(huán)境描述（例如類型規(guī)格）與協(xié)議的定義是分開的。環(huán)境描述的內(nèi)容和說明取決于分析工具。然而，CAPSL中不提供語法、關(guān)鍵字和組織，所以不同的工具都能夠采用CAPSL分析器。名字主體和其他常量的聲明可CAPSL環(huán)境中，協(xié)議會話也能被定義。CAPSL環(huán)境允許聲明多個(gè)協(xié)議會話實(shí)例，BMFBMF（VisualBMF，BMF分析引擎（BMFEngineBMBMFEngineBMFBMFBMFBMFBMFVisual操作。BMFBMFBMFBMFBMFBMFVisualBMFBMF分析工具的一個(gè)用戶界面友好的初始信息輸入接口，輸入組件包入?yún)f(xié)議的安全目標(biāo)配置，如UA-安全，MA-安全，UK-安全和MK-安全。BMF分析引擎支持信任多集中術(shù)語、初始假設(shè)、安全目標(biāo)、推理規(guī)則和公理的形式化BMF規(guī)則引擎，是信任多集擴(kuò)充規(guī)則的用戶輸入界面。基于新鮮性原則，信任多集形BMFBMF失指出直接構(gòu)造攻擊的結(jié)構(gòu)。因此，BMF攻擊引擎支持信任多集形式化方法中關(guān)于攻擊的程的復(fù)雜和乏味，為研究者提供一個(gè)用戶界面友好、高效和具有可用性的環(huán)境。BMF分析BMFBMF分析工具中可視的BMF部分，BMF分析引擎部分和BMF分析結(jié)果顯示部分的部分功能。信任類(4個(gè)子類：主體的信任子類、新鮮性標(biāo)識符的信任子類、密鑰的信任子類、主體知道某密鑰的信任子類)等，參見圖9.2。視化的輸入界面以及分析結(jié)果的顯示，參見圖9.3。戶而獨(dú)立變化。例如，關(guān)聯(lián)性規(guī)則類(6個(gè)子類：雙方共享長期密鑰子類、與可信第三BMF2[30]PrologProlog作為一種實(shí)現(xiàn)語言具有簡單、可靠的特點(diǎn)。BMF2與SPEARII框架[7]GYNGER類似。BMF分析引擎（BMFGER）和結(jié)果顯示界面（BMF結(jié)果顯示SPEARII中的GNYGYNGERPrologBMFGER也采用前向鏈推導(dǎo)技術(shù)，通過對初BMFBMF的結(jié)果顯以Prolog風(fēng)格的信任多集形式化語句保存。信任多集形式化語句采用樹形結(jié)構(gòu)來表示，與將要分析的協(xié)議有關(guān)的消息和初始假設(shè)采用fact/3謂詞的形式來表示，而協(xié)議安全目標(biāo)用goal/2謂詞的形式來表示。對于每個(gè)成功的安全目標(biāo)，BMF結(jié)果顯示部分將Prolog風(fēng)格表示的信任多集分析結(jié)果，參見圖9.4和圖9.5。圖 BMF分析工具2用戶界圖 BMF分析工具2分析結(jié)BMF分析工具的焦點(diǎn)是提供一個(gè)用戶易用，有效且強(qiáng)大的工作環(huán)境，它基于可信任新9.2.22BMF分析工2BMFPrologBMF分析引擎，基于面向?qū)ο蟮姆椒ㄊ褂肑ava源代碼開發(fā)可視的BMFBMF結(jié)果顯示。下最流行的人工智能語言之一，有許多免費(fèi)的和商業(yè)的開發(fā)工具可用。Prolog編程邏輯用關(guān)系表示BMF，代表事實(shí)和規(guī)則，分析是在這些關(guān)系上運(yùn)行一個(gè)查詢而開始的。Prolog很適Java是一種面向?qū)ο蟮募夹g(shù)，使用它的目的是方便源代碼的擴(kuò)展和理解。Java在開發(fā)和調(diào)試用戶易用界面（BMFBMF結(jié)果顯示等）時(shí)具有明確、方便等優(yōu)點(diǎn)。BMFGNY進(jìn)行安全性分析，進(jìn)而實(shí)現(xiàn)分析引擎，并在SPEARIIBMF分析工具在結(jié)構(gòu)和安BMFProlog風(fēng)格的BMF語法，通過可視的BMF界面指定協(xié)議的消息、初始假設(shè)和協(xié)議安全目標(biāo)。隨后基于PrologBMF規(guī)則在分析中被導(dǎo)入并使用，前向鏈推導(dǎo)引擎能夠由初始假設(shè)集合、消息步BMF信任。指定的安全目標(biāo)若獲得成功，BMF分析工具就會生成一個(gè)英語語義風(fēng)格的證明序列并顯示給研究人員。這種BMF分析工具是可擴(kuò)展的，它允許對協(xié)議進(jìn)行擴(kuò)展的安全性分析以滿足將來的需要，因?yàn)橥评硪?guī)則庫是獨(dú)立于BMF分析工具存儲的。出于簡潔考慮，BMF分析工具中涉及的概念下面只進(jìn)行簡單介紹。有興趣的讀者，請假設(shè)必須以fact/3謂詞形式在Prolog文件中進(jìn)行說明。包括理想化的協(xié)議消息、初始假設(shè)，術(shù)語和中間結(jié)論。最后一個(gè)參數(shù)Reason(PremiseList，Rule)fact/3PremiseListfact/3子句所使用的其他fact/3Rulefact/3的分析StatementPremiseListRule將是‘Term’([],‘和分別表示主體‘IdentityStepStatement，整數(shù)‘Step’表示fact/3Index升序插入到事實(shí)getMaxFactIndex/1fact/3的索引為了執(zhí)行一個(gè)基于信任多集形式化方法的協(xié)議安全性分析，設(shè)計(jì)者必須知道什么是所fact/3，協(xié)議的安全目標(biāo)goal/2謂詞來表示，并存儲在目標(biāo)庫中。goal/2謂Indexgoal/2Statement表示預(yù)期的安全性目標(biāo)（信任多集中的安全屬性，包括主體的信任和新鮮性標(biāo)識符的信任。信任用謂詞BeliefBelief(Identity,3信任多集方法中的推理規(guī)則用謂詞rules/0表示，存儲于規(guī)則庫中。對于每一個(gè)BMFrules/0謂詞的實(shí)例，其中有些規(guī)則由于存在多個(gè)結(jié)論而需要更多實(shí)例。PrologaddedFacts原子也被插入到事實(shí)加入了Prolog數(shù)據(jù)庫。A1(a){KN,N'K B( PP)B(<K1NK>)B(:{KN,N'K PiPji rulesfact(PremiseIndex1,told(P,encrypt(List,shared(K))),-),islist(List),length(List,LengthOfList),LengthOfList>1,fact(PremiseIndex2,believes(P,secret(shared(K))),-),fact(PremiseIndex3,believes(P,fresh(shared(K))),-),fact(PremiseIndex4,believes(P,associate(shared(K),P,Q)),-),listMemberIsFresh(P,List,PremiseIndex5),Conclusion=believes(P,bound(List)),not(fact(,Conclusion,-)),SPEARIIBMF環(huán)境使用樹狀結(jié)構(gòu)表示BMF語句，并結(jié)合彈出菜單以便于人機(jī)交互，產(chǎn)生BMF信息的一個(gè)有意義的表示。BMFBMF語句由獨(dú)立的樹概念，盡管要能更有效地使用BMF分析工具他們最好能熟悉BMF邏輯。議將被翻譯成圖形顯示，如圖9.6所示：1.1.{A,3.2.{Na,NbBA圖.9.6密碼協(xié)議在BMF分析工具的表示這里，主體Alice用A表示，主體BobB表示。讀密碼讀密碼ABKAB是與通信參與主體A和B關(guān)聯(lián)的.A(B)KAS(KBS是長期密A(B)知道KAS(KBSABKa1Kb1是保密9.7 是協(xié)議中應(yīng)用的密碼機(jī)制的標(biāo)志：cipherFlag=1， 9.8和MK安全。協(xié)議目標(biāo)以goal/2謂詞形式表示，即Belief(Identity,Trust)。信任Trust是關(guān)于安全屬性的謂詞，包括Existing(Identity),Secret(Identifier),Fresh(Identifier)和Associate(Identifier,Identity)。謂詞Existing(Identity)表示一個(gè)主體擁有關(guān)于這個(gè)主體Identifier的確參與通信的信任。謂詞Secret(Identifier)表示一個(gè)主體擁有關(guān)于這個(gè)新鮮性標(biāo)識符Identifier的保密性信任。謂詞Fresh(Identifier)表示一個(gè)主體擁有關(guān)于這個(gè)新鮮性標(biāo)識符Identifier的新鮮性信任，即新鮮性標(biāo)識符Identifier是為這個(gè)協(xié)議新生成的一個(gè)TVP。謂詞Associate(Identifier,Identity)表示一個(gè)主體擁有關(guān)于這個(gè)新鮮性標(biāo)識符Identifier的關(guān)聯(lián)性信.和Belief(A,Secret(kAB)),Belief(A,Fresh(kAB)),Belief(A,Associate(kAB,A))以及Belief(A,Associate(kAB,B))B協(xié)議要實(shí)現(xiàn)的安全目標(biāo)是Belief(B,Existing(A)),Belief(B,Secret(kAB)),Belief(B,Fresh(kAB)),Belief(B,Associate(kAB,A))以及Belief(B,Associate(kAB,B))。BMFPrologBMF分BMF的自動化分析之前，和協(xié)議相關(guān)的要分析的消息、術(shù)語和初始假設(shè)已BMF分發(fā)送者讀取接收者讀取圖 的，并顯示‘FAILED!’。BMF規(guī)則引擎為新增加的信任多集形式化方法推理規(guī)則的輸入提供了一個(gè)圖形化的環(huán)BMF分析引擎中使用的推理規(guī)則進(jìn)行擴(kuò)rules:-fact(PremiseIndex1,Statement1ToBeInserted,-),...not(fact(-,Conclusion,-)),getMaxFactIndex(MaxIndex),NewIndexisMaxIndex+1,PremiseIndices=[PremiseIndex1,PremiseIndex2,...],將信任多集形式化方法中的新推理規(guī)則轉(zhuǎn)換為Prolog格式的BMF分析工具中的推理規(guī)則。用信任多集形式化方法中新推理規(guī)則的條件替換Statement1ToBeInserted,Statement2ToBeInserted等。用信任多集形式化方法中新推理規(guī)則的結(jié)論替換ConclusionToBeInserted；用新推理規(guī)則的名字替換RuleNameToBeInserted。fact/3謂詞指定這個(gè)規(guī)則的所有初始假設(shè)，PrologProlog是一種與人工智能相關(guān)的程根據(jù)信任多集形式化方法對協(xié)議進(jìn)行安全性分析得來的安全屬性缺失，BMF攻擊引擎支持任新鮮性方法構(gòu)造攻擊的攻擊引擎，如圖9.10所示。B(A)構(gòu)造“攻擊”：圖 5；如果N-S協(xié)議的安全性分析，AB在這個(gè)協(xié)議運(yùn)行中的確參與了通信，并且共NANBABB相B沒有得到任何確鑿的證據(jù)來證明NAAB相關(guān)聯(lián)。Message I(A)→ {A,NAMessage1 I(A)→B: {A,NA}KBMessage B→ {NA,NBMessage I(A)→ A所以無法得到新鮮性標(biāo)識符NB。AA如果攻擊者I想要生成消息{NB}KB，I必須知道NB。由于NB只出現(xiàn)在消息2和消息3中，AIIMessage ??→ {Message A→ {MessageA{A,??}Message{??,NB}MessageA到NB只能重放記錄的包括{??,NB}KA的消息2{NA,NB}KA給A，即Message “??”Message A {A,NAMessage1 I(A)→B: {A,NA}KBMessage B→ {NA,NBMessage I(A)→ Message1’ A→I: {A,NA}KIMessage2’ Message3’ A→I:

MessageA{A,NAMessageI(A)→{A,NAMessageB→{NA,NBMessage{NA,NBMessageAMessageI(A)→ {A,N {A,NA{A,NA 3’. AB共享了秘密隨機(jī)數(shù)NA和NB，以生成新的會話密鑰。DongL,ChenK,ZhengY,HongX(2008)TheGuaranteeofAuthenticationProtocolSecurity.JournalofShanghaiJiaoTongUniversity,42(4):518–522(inChinese)ChenK,DongL,LaiX(2008)SecurityAnalysisofCryptographicProtocolsBasedonTrustedFreshness.JournalofKoreaInstituteofInformationSecurityandCryptology,18(6B):1–13DongL,ChenK,LaiX(2009)BeliefMultisetsforCryptographicProtocolAnalysis.JournalofSoftware,20(11):3060–3076(inChinese)DongL,ChenK,LaiX,WenM(2009)WhenisaKeyEstablishmentProtocolSecurityandCommunicationNetworks,2(6):567–SaulE(2001)FacilitatingtheModellingandAutomatedAnalysisofCryptographicMasterThesis,UniversityofCapeMaoW(2004)ModernCryptography:TheoryandPractice.PrenticeHall,NewSaulEandHutchisonA(1999)SPEARII:TheSecurityProtocolEngineeringandAnalysisResource.SecondSouthAfricanTelecommunications,Networks,andApplicationsAccessed9JulyBekmannJ,GoedeP.deandHutchisonA(1997)SPEAR:aSecurityProtocolEngineering&AnalysisResource.InDIMACSWorkshoponDesignandFormalVerificationofSecurityProtocols./Workshops/Security/program2/hutch/spear.html.Accessed9JulyBurrowsM,AbadiM,andNeedhamR(1990)Alogicofauthentication.ACMTransactionsonComputerSystems,8(1):18–36LoweG(1996)BreakingandFixingtheNeedham-SchroederPublic-keyProtocolFDR.In:TACAS’96Proceedingsofthe12thInternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems,Passau,27–29Mar1996.LectureNotesinComputerScience(LectureNotesinSoftwareConfigurationManagement),vol1055.Springer-Verlag,Heidelberg,pp147–166LoweG(1995)AnAttackontheNeedham-SchroederPublicKeyAuthenticationInformationProcessingLetters,56(3):131–133,LoweG(1996)SomenewAttacksUponSecurityProtocols.InProceedingsofthe9thIEEEComputerSecurityFoundationsWorkshop,pages162–169,Jun.1996RoscoeAW(1994)ModelCheckingCSP.In:RoscoeAW(ed)AClasicalMind:EssaysinHonourofC.A.RHoare.Prentice-Hall,1994MeadowsC(1996)TheNRLProtocolAnalyzer:anOverview.JournalofLogicProgramming,26(2):113–131DolevD,YaoAC(1983)OntheSecurityofPublicKeyProtocols.IEEETransactionsonInformationTheory29(2):198–208MeadowsC(1994)AModelofComputationfortheNRLProtocolAnalyzer.In:Proceedingsofthe1994ComputerSecurityFoundationsWorkshop,Franconia,14–16June1994HarkinsDandCarrelD(1998)TheInternetKeyExchangeProtocol(IKE).IETFRFC2409,/rfc/rfc2409.txt.Accessed9July2012KaufmanC(2005)InternetKeyExchange(IKEv2)Protocol.IETFRFC4306,/html/rfc4306.Accessed9July2012SET(1997)SecureElectronicTransaction.TheSETStandardSpecification./set/.Accessed9July2012MitchellJ.C,MitchellMandSternU(1997)AutomatedAnalysisofCryptographicUsingMurΦ.Proc.of1997IEEESymposiumonSecurityandPrivacy,Oakland,California,pp141–153NeedhamRM,SchroederMD(1978)UsingEncryptionforAuthenticationinLargeNetworkofComputers.CommunicationoftheACM21(12):993–999Tatebayashi