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

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

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

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

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