包含XOR的安全協(xié)議自動(dòng)驗(yàn)證的改進(jìn).pdf

1、安全協(xié)議通常描述了公共網(wǎng)絡(luò)中兩個(gè)或多個(gè)智能進(jìn)程之間的消息交換行為，從而保證對(duì)交互過(guò)程中諸如認(rèn)證、機(jī)密保持、密鑰一致、隱私和匿名性等安全屬性的支持。但是，設(shè)計(jì)一個(gè)安全可信的協(xié)議并不是一件容易的事情，而這些不安全的協(xié)議往往就系統(tǒng)攻擊的入口點(diǎn)。從Lowe[1]提出了形式化自動(dòng)驗(yàn)證之后，該驗(yàn)證方法已經(jīng)展示了其在協(xié)議安全性證明方面的強(qiáng)大優(yōu)勢(shì)并得到了廣泛的應(yīng)用。
　　 由于針對(duì)密碼學(xué)原語(yǔ)具體算法的攻擊往往難以分析，以自動(dòng)化的形式證明攻擊就更

2、加困難，因此密碼學(xué)操作原語(yǔ)在形式化驗(yàn)證中往往被看作是不帶任何代數(shù)屬性的函數(shù)符號(hào)，忽略其具體計(jì)算細(xì)節(jié)，這個(gè)假設(shè)被稱(chēng)為完美密碼假設(shè)證[2]，也就是說(shuō)加密后的消息除非使用相應(yīng)的密鑰解密打開(kāi)，否則是不可能通過(guò)其他方式得到其對(duì)應(yīng)明文的?；谶@個(gè)假設(shè)，目前存在很多自動(dòng)化驗(yàn)證工具，其中ProVerif[3]以其高效的性能被公認(rèn)為目前最優(yōu)秀的驗(yàn)證工具之一[4]。但是，ProVerif等上具沒(méi)有涵蓋那些利用密碼學(xué)操作原語(yǔ)代數(shù)屬性的攻擊。因此，完美假設(shè)的限

3、制需要適當(dāng)放寬，從而將此類(lèi)攻擊有效的識(shí)別出來(lái)。
　　 位運(yùn)算符XOR(exclusive or)廣泛應(yīng)用于最近幾年流行的RFID協(xié)議中，再加上其簡(jiǎn)潔的格式，已經(jīng)成為目前的研究熱點(diǎn)。因此，為了能夠更加有效的發(fā)現(xiàn)包含有XOR安全協(xié)議的攻擊隱患，需要將對(duì)操作符代數(shù)屬性的使用能力加入到入侵者的攻擊能力中。
　　 特里爾大學(xué)的Kusters教授和Truderung最近提出了一個(gè)對(duì)包含有操作符XoR(O）安全協(xié)議的自動(dòng)驗(yàn)證方法。在該

4、方法中，包含有XOR的協(xié)議模型被自動(dòng)轉(zhuǎn)換為相應(yīng)的可進(jìn)行形式化驗(yàn)證的等價(jià)模型，其中已經(jīng)包含了對(duì)XOR的代數(shù)屬性運(yùn)算的合理建模，該等價(jià)模型可以作為ProVerif的輸入模型，由它自動(dòng)驗(yàn)證。雖然該方法在驗(yàn)證機(jī)密性時(shí)表現(xiàn)出較高效率但是在認(rèn)證屬性的驗(yàn)證中往往效率不高，對(duì)某些協(xié)議甚全無(wú)法處理。
　　 本文中，針對(duì)Kusters和Truderung算法存在的缺陷，提出了兩個(gè)改進(jìn)方向：第一，為了擴(kuò)展可驗(yàn)證認(rèn)證屬性的安全協(xié)議的范圍，提出了有界驗(yàn)證