密碼協(xié)議的安全性分析技術研究.pdf

1、隨著網(wǎng)絡技術的迅速普及與發(fā)展,網(wǎng)絡中敏感信息的保護已變得越來越重要。密碼協(xié)議正是為通信的雙方或多方提供這樣的安全保證。然而,由于網(wǎng)絡本身的開放性,其中存在著嚴重的安全威脅,攻擊者可以通過各種方式對密碼協(xié)議進行攻擊,破壞其安全特性。因此,對密碼協(xié)議進行安全性分析至關重要。
　　 本文按照密碼協(xié)議不同的應用環(huán)境將其分為兩種,一種是應用于傳統(tǒng)計算機網(wǎng)絡的密碼協(xié)議,這種協(xié)議在設計時不必考慮密碼原語的復雜度,僅以保證協(xié)議的安全性為目標,稱

2、為傳統(tǒng)密碼協(xié)議；另外一種是應用于RFID系統(tǒng)的密碼協(xié)議,這種密碼協(xié)議由于受到標簽成本限制,在設計時必須采用結(jié)構(gòu)簡單、計算復雜度低的密碼原語,并利用他們的代數(shù)性質(zhì)進行代數(shù)運算和等式推導來實現(xiàn)協(xié)議的安全目標,稱為輕量級協(xié)議。當前,對這兩種協(xié)議的分析方法也有所不同:針對傳統(tǒng)的密碼協(xié)議,一般采用形式化方法。形式化方法具有嚴格、明確、清晰和反直覺等特點,因此是分析密碼協(xié)議的有效工具,但由于其抽象化程度太高,不能分析帶有代數(shù)運算和等式推導的協(xié)議,因

3、此對于應用于RFID系統(tǒng)的輕量級協(xié)議,只能采用手工驗證方法。本文對這兩種方法都進行了研究,對于傳統(tǒng)的密碼協(xié)議,研究了基于SAT模型檢測的方法,并對該方法進行了功能擴展；對于輕量級協(xié)議,采用手工驗證方法,分析了兩個優(yōu)秀的輕量級協(xié)議的安全性,找到了兩個獨特的攻擊。本文的主要研究成果如下:
　　 (1)提出了一個新的可以檢測類型缺陷攻擊的模型SAT-1。該模型通過在匹配模式中引入無類型變量,并通過無類型消息的概念,解除了原SAT模型檢

4、測器對未知消息的類型限制。同時,通過增加消息匹配算法,使誠實主體能夠接受帶有類型缺陷的消息,從而實現(xiàn)了類型缺陷攻擊的檢測。在對Otway-Rees協(xié)議的檢測中,不僅發(fā)現(xiàn)了已有的針對發(fā)起者A的類型缺陷攻擊,而且發(fā)現(xiàn)了新的針對響應者B的類型缺陷攻擊,證明了SAT-1模型的可靠性。
　　 (2)針對當前模型檢測工具普遍不能檢測帶有異或運算密碼協(xié)議的問題,提出了一個新的模型SAT-2。該模型通過引入抽象異或項的概念及其運算規(guī)則,大大降低

5、了攻擊者生成的異或消息數(shù)量,解決了由于引入異或運算所導致的狀態(tài)空間爆炸問題。在此基礎上,通過在SAT模型中增加基于抽象異或項的重寫規(guī)則,擴展了攻擊者的異或運算能力,實現(xiàn)了對帶有異或運算密碼協(xié)議的自動化檢測。最后通過對BULL協(xié)議的檢測,證明了抽象異或項的實用性,同時也證明了SAT-2模型檢測器的可靠性。
　　 (3)設計了一個多協(xié)議攻擊自動化檢測系統(tǒng)ADMA。該系統(tǒng)由協(xié)議搜索子系統(tǒng)和攻擊確認子系統(tǒng)兩部分組成。協(xié)議搜索子系統(tǒng)根據(jù)多

6、協(xié)議攻擊中目標協(xié)議與輔助協(xié)議加密消息類型一致性的條件,自動化搜索可能對目標協(xié)議構(gòu)成威脅的候選輔助協(xié)議。攻擊確認子系統(tǒng)通過改進的SAT模型檢測方法,自動化確認目標協(xié)議與候選輔助協(xié)議是否存在多協(xié)議攻擊。試驗結(jié)果表明,ADMA系統(tǒng)能夠?qū)崿F(xiàn)多協(xié)議攻擊的自動化檢測,并且檢測中發(fā)現(xiàn)了新的多協(xié)議攻擊。
　　 (4)提出了一個可變攻擊者模型構(gòu)造方案CIM。該方案利用異或運算,阿貝爾加法群運算以及阿貝爾乘法群運算的代數(shù)性質(zhì),定義了抽象項的概念及其

7、運算規(guī)則,大大降低了攻擊者進行代數(shù)運算的復雜度。在此基礎上,將攻擊者所有的攻擊行為轉(zhuǎn)化為重寫規(guī)則,并定義了攻擊者行為庫和攻擊規(guī)則選擇算法,使檢測者能夠根據(jù)不同的協(xié)議選擇并組合不同的攻擊行為,構(gòu)造可變的攻擊者模型。與傳統(tǒng)固定的攻擊者模型方案相比,該方案能夠根據(jù)不同的協(xié)議動態(tài)調(diào)整攻擊者模型,并且能夠降低攻擊者執(zhí)行代數(shù)運算的復雜度,因此保證了協(xié)議分析的效率和準確性。
　　 (5)針對Lee等人提出的應用于RFID系統(tǒng)的身份傳輸協(xié)議,提

8、出了一個獨特的三會話攻擊。在該三會話攻擊中,攻擊者利用第一個會話監(jiān)聽目標標簽和閱讀器之間傳遞的消息,然后利用第二個會話收集目標標簽的響應信息,最后通過第三個會話發(fā)動中間人攻擊并對目標標簽進行追蹤,破壞了協(xié)議的不可追蹤性。與傳統(tǒng)的兩會話攻擊相比,三會話攻擊更難于發(fā)現(xiàn)并且對攻擊者要求更高,因此對三會話攻擊進行了可行性分析,指出了其攻擊成功的條件。
　　 (6)發(fā)現(xiàn)了三個針對Kulseng等人提出的應用于RFID系統(tǒng)的互認證協(xié)議的攻擊