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

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

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

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

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