安全協(xié)議-第6章-上_第1頁
安全協(xié)議-第6章-上_第2頁
安全協(xié)議-第6章-上_第3頁
安全協(xié)議-第6章-上_第4頁
安全協(xié)議-第6章-上_第5頁
已閱讀5頁,還剩37頁未讀, 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報(bào)或認(rèn)領(lǐng)

文檔簡介

安全協(xié)議分析與設(shè)計(jì)

第六章(上)衛(wèi)劍釩安全協(xié)議的設(shè)計(jì)在設(shè)計(jì)安全協(xié)議時(shí),如果稍有不慎,就可能使協(xié)議存在安全隱患。有鑒于此,Abadi和Needham提出了設(shè)計(jì)認(rèn)證協(xié)議的若干原則[AN96]。值得注意的是,這些原則只是非形式化的設(shè)計(jì)指導(dǎo),它們既不是認(rèn)證協(xié)議安全的充分條件也不是必要條件[Syve96]。一些工作致力于將形式化方法結(jié)合到協(xié)議的設(shè)計(jì)中,典型的方法有:Heintze-Tygar

方法[HT94],Gong和Syversion

的fail-stop協(xié)議[GS95],Buttyan&Staamann的簡單邏輯[BSW98],Canetti和Krawczyk的CK方法[CK01]等等。一些方法則通過窮舉來搜索所有可能的安全協(xié)議,然后進(jìn)行分析驗(yàn)證以得到安全協(xié)議。最后一節(jié)探討如何設(shè)計(jì)具有防范DoS攻擊能力的安全協(xié)議。2安全協(xié)議設(shè)計(jì)的基本原則這些原則最初是由MartinAbadi和RogerNeedham提出來的[AN94,AN96],RossAnderson和RogerNeedham在文獻(xiàn)[AN95]中又專門針對公開密鑰協(xié)議提出了一系列設(shè)計(jì)原則。這些設(shè)計(jì)原則既不能保證安全,同時(shí)也不是達(dá)到安全的必要條件,但它們的確能夠有效地防止一些常見的攻擊。3基本原則含義明確原則原則1每條消息都能清楚地表達(dá)它的意思,對消息的解釋必須完全依賴于消息的內(nèi)容。形象地說,每一條消息都能用一句明明白白的語句來替代。例如,服務(wù)器S發(fā)出一條消息:{P,S,A,B,Kab}KA。這條消息可以表述為“在接收到P以后,S向A發(fā)送一個(gè)A與B之間通信的密鑰K-ab”,這句話中的所有內(nèi)容都必須在協(xié)議中顯式地表達(dá)出來,使得消息的接收者根據(jù)協(xié)議中的信息就可以清楚地知道這條消息的含義,而不需要從上下文中推導(dǎo)。因?yàn)槿绻硞€(gè)信息需要從上下文中推導(dǎo),那么攻擊者就可能通過在上下文中加入欺詐的信息來擾亂協(xié)議的正常運(yùn)行。4基本原則聲明條件原則原則2對消息適用的條件要清楚地說明,以便協(xié)議的使用者能夠根據(jù)這些條件判斷是否采用該協(xié)議。例如,某人希望采用公鑰加密體制為基礎(chǔ)的安全協(xié)議,他就可以選用類似NSPK這樣的協(xié)議而不是NSSK協(xié)議;同樣地,如果他希望第三方產(chǎn)生密鑰,就不會選取大嘴青蛙協(xié)議。此外,保密原則也是一個(gè)基本原則,即不以明文的形式傳遞任何私有密鑰以及其他秘密信息,這一點(diǎn)通常是容易做到的。5命名原則命名原則原則3如果主體的身份是一個(gè)關(guān)鍵消息,那么消息中應(yīng)該明確標(biāo)示主體的名字。這可看做是原則1的一個(gè)特例,但由于不符合這條原則帶來的問題太多,故而專門列作一條原則。值得注意的是,不包含主體的名字不一定帶來問題,但作為謹(jǐn)慎的做法,最好還是帶上主體的名字。6加密原則原則4明白為什么需要加密。濫用加密會導(dǎo)致運(yùn)算成本提高和協(xié)議冗余,而且加密并不總是意味著安全,不恰當(dāng)?shù)募用苡袝r(shí)還會導(dǎo)致錯(cuò)誤。早期的Kerberos協(xié)議[MNSS87]基于NSSK協(xié)議,但使用時(shí)間戳替換了Nonce,簡化如下:7Msg1是不需要加密的,Msg2需要加密,因?yàn)镸sg2中包含了S分配給A和B的通信密鑰Kab。使用Kas能夠讓A知道這是S發(fā)出的,有一定的簽名意義。但Msg2中是否需要雙重加密?這種做法是從NSSK中繼承來的,但雙層的加密并沒有給機(jī)密性和認(rèn)證性帶來任何附加的好處,相反,它增加了運(yùn)算量。也許有人說這樣可以使B在收到Msg3后得知A一定收到了Msg2,但這種解釋不太尋常,也未必是協(xié)議設(shè)計(jì)者的本意(后繼的Kerberos版本中去掉了這個(gè)雙重加密)。8原則5先簽名后加密主體對一個(gè)加密了的消息進(jìn)行簽名是不可靠的,因?yàn)橹黧w可能并不知道明文是什么;而如果先簽名后加密,一方面表明主體認(rèn)可該消息,另一方面還保證了機(jī)密性。不滿足這個(gè)原則有時(shí)會導(dǎo)致協(xié)議的錯(cuò)誤,如在X.509系列協(xié)議中的單消息協(xié)議。9圖中Ta是時(shí)間戳,Na是隨機(jī)數(shù)(但通常并不使用),Xa和Ya是用戶數(shù)據(jù),協(xié)議的目的是保證Xa和Ya的完整性,讓B得知Xa和Ya的產(chǎn)生者為A,并保證數(shù)據(jù)Ya的機(jī)密性。這個(gè)協(xié)議的問題在于,B事實(shí)上并不能保證主體A知道Ya的內(nèi)容,[AN96]認(rèn)為協(xié)議存在類似對Denning-Sacco協(xié)議的攻擊,一個(gè)主體C把Msg1中A的簽名去掉,然后換成C自己的簽名發(fā)送給B,B會認(rèn)為C認(rèn)可了Ya,而事實(shí)上C并不知道Ya的內(nèi)容。10這個(gè)原則僅僅是一個(gè)指導(dǎo)性的原則,一些不滿足這個(gè)原則的協(xié)議仍然是安全的,如下圖所示的ISO/IEC11770-3密鑰傳送協(xié)議。11時(shí)間性原則原則6設(shè)計(jì)者應(yīng)該清楚地知道在使用Nonce時(shí)所要保證的性質(zhì)。以O(shè)tway-Rees協(xié)議為例:12時(shí)間性原則在這個(gè)協(xié)議中,M是協(xié)議運(yùn)行的會話標(biāo)識符,新的會話密鑰Kab由可信第三方S產(chǎn)生,Na和Nb不僅起到了保證新鮮性的作用,還起到了綁定主體名的作用。但是協(xié)議略顯冗余,文獻(xiàn)[AN96]中建議將其簡化,使其含義更為明確13時(shí)間性原則原則7通過計(jì)數(shù)器來保證新鮮性時(shí),需要注意對其進(jìn)行秘密性保護(hù)。如果Na是Nonce的話,協(xié)議是安全的,但若Na是計(jì)數(shù)器這種可預(yù)測的量,協(xié)議就不安全了。14時(shí)間性原則攻擊者C可以產(chǎn)生Na的下一個(gè)取值Na+1,將其發(fā)給S,然后從S那里得到一個(gè)包含系統(tǒng)時(shí)鐘的消息,當(dāng)A使用Na+1來獲取時(shí)間的時(shí)候,C就可以把這個(gè)保存的消息傳給A,這樣A的系統(tǒng)時(shí)間就不準(zhǔn)確了。協(xié)議可以修改如下:15時(shí)間性原則原則8如果采用時(shí)間戳來保證新鮮性,那么系統(tǒng)中的時(shí)間差異應(yīng)該遠(yuǎn)小于消息的有效生存時(shí)間。系統(tǒng)的時(shí)間同步機(jī)制應(yīng)該是系統(tǒng)可信計(jì)算基的一部分。比如在Kerberos協(xié)議中,系統(tǒng)時(shí)間比較慢的主體經(jīng)常會有很多問題,它經(jīng)常會把一個(gè)已經(jīng)過期的證書當(dāng)做有效的證書使用;同樣,一個(gè)走得過快的時(shí)鐘有時(shí)候也會為攻擊者提供機(jī)會,如主體A(時(shí)鐘過快的主體)在時(shí)間點(diǎn)T0發(fā)送了一個(gè)時(shí)間戳為T(T0<T)的消息,那么攻擊者C就可以在時(shí)間點(diǎn)T附近重放這個(gè)消息而不被察覺。16時(shí)間性原則原則9對Nonce或時(shí)間戳這種新鮮性數(shù)值的加密不意味著密鑰的新鮮性。NSSK協(xié)議中,對B來說,當(dāng)收到Msg5后,可以肯定Kab是剛剛被使用過的密鑰,但是這并不能保證Kab的新鮮性,也即不能保證Kab是剛剛被產(chǎn)生出來的。17識別原則原則10通常情況下每種協(xié)議都有自己的消息格式,主體收到一條消息后,應(yīng)該能從消息格式中判斷出該消息是屬于哪個(gè)協(xié)議,屬于哪次運(yùn)行,以及它是第幾條消息。考察NSSK協(xié)議的Msg4和Msg5:Msg4 B→A:{Nb}KabMsg5 A→B:{Nb+1}Kab

Msg5中把Nb加上1,其目的是防止攻擊者對Msg4的重放,事實(shí)上,只要能夠表達(dá)這種意義的消息都被認(rèn)為是可行的,區(qū)分這兩條消息的方法有很多,比如寫成如下的形式:Msg4 B→A:{NSSK,“Message4”,Nb}KabMsg5 A→B:{NSSK,“Message5”,Nb}Kab18信任原則原則11協(xié)議的設(shè)計(jì)者應(yīng)該知道他所設(shè)計(jì)的協(xié)議是基于怎樣的信任關(guān)系,為什么要基于這種信任,以及有沒有把握保證這種信任的存在。比如在Kerberos協(xié)議中,服務(wù)器及其時(shí)間源應(yīng)該被信任,如果服務(wù)器發(fā)出錯(cuò)誤的時(shí)間戳,則整個(gè)系統(tǒng)的安全性都不能得到保證。再如大嘴青蛙協(xié)議,協(xié)議由A產(chǎn)生會話密鑰Kab,這種信任關(guān)系是否能被接受?主體A是否能保證產(chǎn)生的密鑰具有保密性、不可重復(fù)性和不可預(yù)測性?這需要協(xié)議設(shè)計(jì)者審慎地加以考慮。19安全協(xié)議的設(shè)計(jì)方法研究fail-stop協(xié)議CK模型20fail-stop協(xié)議Gong&Syverson在文獻(xiàn)[GS95]中提出了fail-stop協(xié)議的概念,其含義為:當(dāng)遭遇任何干擾協(xié)議正常執(zhí)行的主動功擊時(shí),協(xié)議將立即停止。它可以使協(xié)議設(shè)計(jì)更加容易,并對協(xié)議分析方法的要求大為降低。[GS95]認(rèn)為,一個(gè)分布式的系統(tǒng)可視為一些空間上分離的進(jìn)程的集合,它們通過交換消息來進(jìn)行通信;協(xié)議是對所交換的消息的格式與相應(yīng)時(shí)間的一個(gè)說明;安全協(xié)議使用密碼體制,如加密算法和解密算法,來保證消息的完整性、秘密性、消息源發(fā)點(diǎn)、消息目的地、消息順序以及消息意義;消息是被一步一步(step)執(zhí)行的。21fail-stop協(xié)議定義6.1

fail-stop協(xié)議:如果某個(gè)協(xié)議能夠做到這一點(diǎn),即若攻擊者對協(xié)議中某條消息的發(fā)送進(jìn)行了干擾(如偽造、篡改、重放、插入、截?cái)嗟龋?,則協(xié)議后繼的消息不再發(fā)送,那么這個(gè)協(xié)議是fail-stop協(xié)議。為方便起見,有時(shí)也稱fial-stop協(xié)議中某條消息是fial-stop的。定義6.1是非形式化的,這是為了能夠更直觀地對fail-stop概念進(jìn)行描述22斷言6.1主動攻擊不會導(dǎo)致fail-stop協(xié)議在運(yùn)行時(shí)秘密泄露。由于主動攻擊可導(dǎo)致一個(gè)fail-stop協(xié)議的停止,因此一個(gè)主動攻擊者并不能獲得比被動攻擊者更多的信息。23抵御被動攻擊的分析一個(gè)fail-stop協(xié)議是否可以抵御被動攻擊?證明分為3個(gè)階段:階段1驗(yàn)證協(xié)議的fail-stop性質(zhì),即判斷該協(xié)議是否是一個(gè)fail-stop協(xié)議;階段2驗(yàn)證秘密假設(shè),分析一個(gè)被動攻擊者是否可以得到協(xié)議中的秘密;階段3在階段2的基礎(chǔ)上,應(yīng)用BAN類邏輯分析協(xié)議。24階段1.驗(yàn)證fail-stop性質(zhì)階段1.驗(yàn)證fail-stop性質(zhì)驗(yàn)證一個(gè)協(xié)議是否為fail-stop協(xié)議,最直接的辦法是驗(yàn)證協(xié)議與一個(gè)fail-stop協(xié)議規(guī)范是一致的??赡軙泻芏喾Nfail-stop協(xié)議規(guī)范,這里先給出一種簡單的fail-stop協(xié)議規(guī)范,這類協(xié)議使用對稱密碼體制。斷言6.2如果滿足下述條件,則一個(gè)協(xié)議是fail-stop的。(1)每個(gè)消息含有一個(gè)消息頭,內(nèi)含發(fā)送者標(biāo)識、接收者標(biāo)識、協(xié)議標(biāo)識及協(xié)議版本號、消息序號以及一個(gè)新鮮性標(biāo)識。(2)每個(gè)消息都是被加密的,加密密鑰是發(fā)送者和接收者之間的共享密鑰。(3)一個(gè)誠實(shí)主體按照協(xié)議運(yùn)行,并忽略所有非預(yù)期的消息。(4)當(dāng)一個(gè)期望的消息在規(guī)定的時(shí)間內(nèi)沒有到達(dá),主體停止運(yùn)行。25階段2.秘密性假設(shè)的驗(yàn)證階段2.秘密性假設(shè)的驗(yàn)證由于主動攻擊將停止一個(gè)fail-stop協(xié)議,攻擊者如果想盡可能多地收集消息,最好還是不加干擾地等協(xié)議運(yùn)行完畢,也即最好做一個(gè)被動攻擊者。驗(yàn)證一個(gè)協(xié)議執(zhí)行是否會泄露秘密,只需確定被動攻擊者能否通過處理消息而獲得特定的數(shù)據(jù)項(xiàng)(簡稱項(xiàng))。給定攻擊者已擁有的項(xiàng),有如下的擁有規(guī)則。(1)擁有一個(gè)項(xiàng),則擁有項(xiàng)中的所有子項(xiàng)。(2)擁有一個(gè)項(xiàng)的所有子項(xiàng),則擁有該項(xiàng)。(3)擁有一個(gè)項(xiàng),則擁有該項(xiàng)的函數(shù)運(yùn)算結(jié)果,前提是該函數(shù)對于攻擊者是可計(jì)算的(如擁有x則擁有Hash(x))。(4)擁有一個(gè)項(xiàng)和一個(gè)加密密鑰,則擁有該項(xiàng)的加密形式,即一個(gè)加密項(xiàng)。(5)擁有一個(gè)加密項(xiàng)和對應(yīng)的解密密鑰,則擁有解密后的項(xiàng)。26階段3.應(yīng)用BAN類邏輯階段3.應(yīng)用BAN類邏輯BAN類邏輯在對協(xié)議進(jìn)行分析時(shí),需要一些前提假設(shè),如要求一個(gè)主體能判斷一個(gè)消息是不是自己發(fā)的,而滿足斷言6.2中定義的fail-stop協(xié)議能自動滿足這個(gè)假設(shè)。此外,對于fail-stop協(xié)議,邏輯中關(guān)于新鮮性驗(yàn)證和可識別性驗(yàn)證(如GNY邏輯)的公理或規(guī)則都可以被簡化或去掉。BAN類邏輯有一個(gè)共同的關(guān)鍵假設(shè):所有秘密在協(xié)議執(zhí)行中是保密的。因此,需要用階段2來驗(yàn)證秘密性假設(shè)。27有些協(xié)議在前部分傳送一個(gè)會話密鑰,后部分用這個(gè)密鑰來握手。協(xié)議的前兩條消息是服務(wù)器S給A和B分發(fā)會話密鑰k,后兩個(gè)消息中,A和B使用該密鑰進(jìn)行握手。在這個(gè)協(xié)議中,后兩條消息中使用的k是前兩條消息中的內(nèi)容,在不能判定k的安全性的情況下,無法認(rèn)定整個(gè)協(xié)議是否是fail-stop的??梢韵葘Φ?條和第2條消息組成的部分進(jìn)行分析,當(dāng)這個(gè)部分通過3個(gè)階段的驗(yàn)證后,就可以得知k是安全的,然后再對整個(gè)協(xié)議進(jìn)行3個(gè)階段的分析。28分析Nessett協(xié)議Nessett協(xié)議這個(gè)協(xié)議不是fail-stop的,因?yàn)橐粋€(gè)攻擊者竊聽到Msg1后,可以把Msg1轉(zhuǎn)發(fā)給誠實(shí)主體C,C得到這個(gè)消息后,不能判斷這個(gè)消息是不是被轉(zhuǎn)發(fā)來的還是確實(shí)是A發(fā)給自己的,而繼續(xù)執(zhí)行協(xié)議。為了使這個(gè)協(xié)議能夠fail-stop,可以在Msg1中添加B的身份,使Msg1成為{B,Na,Kab}Ka?1,這樣,協(xié)議就是fail-stop的了。一個(gè)隱含的假設(shè)是:沒有其他協(xié)議的消息片段和修改后的Msg1有同樣的形式,如果這個(gè)隱含假設(shè)不滿足的話,可以在Msg1中添加協(xié)議標(biāo)識和協(xié)議版本號來區(qū)分。29下面開始第2階段的分析,這個(gè)階段要對秘密保持的假設(shè)進(jìn)行驗(yàn)證。協(xié)議中,Kab是一個(gè)需要保持秘密的量,對它的秘密性不作驗(yàn)證就無法分析Msg2。依據(jù)階段2里提到的5條擁有規(guī)則,可以很容易得出:擁有{B,Na,Kab}Ka?1并且擁有Ka,則擁有{B,Na,Kab};擁有{B,Na,Kab}則擁有Kab。從推理可知,攻擊者能夠擁有Kab,修改Msg1后的Nesset協(xié)議不能通過階段2的驗(yàn)證,協(xié)議無法繼續(xù)后繼的BAN類邏輯分析。30分析大嘴青蛙協(xié)議這個(gè)協(xié)議存在攻擊,是S不能分辨重放的消息。主要的原因在于消息的區(qū)別能力,只要第2條消息能在格式上比第1條消息能有1比特的差異,這個(gè)協(xié)議就是fail-stop的。在將該協(xié)議修改為fail-stop協(xié)議后,可以對其進(jìn)行第2階段的分析,這是容易驗(yàn)證的,只要Kas和Kbs保持秘密,就可以保證協(xié)議的秘密不被泄露。BAN邏輯分析的結(jié)果表明修改后的該協(xié)議是安全的。31CK模型Canetti和Krawczyk在文獻(xiàn)[BCK98]的基礎(chǔ)上,采用復(fù)雜性理論對密鑰交換協(xié)議做了安全特性的定義[CK01],提出了一種模塊化設(shè)計(jì)密鑰交換協(xié)議的理論和方法,這里對其進(jìn)行簡要的介紹。CK模型將安全協(xié)議模型化為n個(gè)主體上運(yùn)行的多個(gè)進(jìn)程,每個(gè)主體可以同時(shí)運(yùn)行協(xié)議的多個(gè)會話。攻擊者控制整個(gè)通信并試圖通過與協(xié)議的交互來獲得秘密,并可以有如下的行為:激活(activate)主體運(yùn)行協(xié)議;攻破(corrupt)主體;主體內(nèi)部狀態(tài)泄漏(reveal);進(jìn)行會話輸出查詢(query)。32AM/UM模型攻擊者能力模型分為AM模型和UM模型,AM模型可被視為理想環(huán)境,在AM模型下攻擊者只能通過傳遞另一個(gè)主體發(fā)送的消息來使主體激活;攻擊者可以選擇不傳遞消息,但一旦傳遞,就只能傳送一次,并且忠實(shí)地傳送到消息預(yù)定目的地;攻擊者可以偽裝網(wǎng)絡(luò)地址,但不能篡改消息和重放消息。UM模型可被視為真實(shí)環(huán)境,UM下攻擊者除了具備AM中的能力外,還可以主動激活主體與另外一個(gè)主體的會話,并可以任意篡改和重放消息。激活的含義是指使一個(gè)主體主動地發(fā)起協(xié)議運(yùn)行,如對于NSPK協(xié)議,攻擊者在需要的時(shí)候,可以使主體A發(fā)起對攻擊者自己的協(xié)議運(yùn)行。33SK安全定義6.2滿足以下條件的認(rèn)證協(xié)議被稱為SK安全:(1)如果兩個(gè)未被攻破的主體完成一次匹配的會話后,它們都接受相同的會話密鑰。(

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

評論

0/150

提交評論