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

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

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

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

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

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

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

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

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