密碼協(xié)議的安全性分析和證明長(zhǎng)期以來(lái)一直是信息安全研究的熱點(diǎn)和難點(diǎn)問(wèn)題，從事計(jì)算機(jī)科學(xué)和密碼學(xué)研究的人員對(duì)此進(jìn)行了不懈的研究，也取得了較為豐碩的研究成果：但是，時(shí)至今日，這個(gè)問(wèn)題仍然沒(méi)有很好地解決。密碼協(xié)議和其他協(xié)議不同，人們也許永遠(yuǎn)無(wú)法知道攻擊者下一步將采取什么樣的攻擊手段，有時(shí)甚至恰恰就是在那些被認(rèn)為相當(dāng)安全的細(xì)節(jié)出現(xiàn)了微妙的漏洞，要知道即便這樣一個(gè)微小的漏洞或缺陷有時(shí)對(duì)于一個(gè)聰明的攻擊者來(lái)說(shuō)已經(jīng)足夠。也許，這也正是密碼協(xié)議安全設(shè)計(jì)和分析的魅力所在。

　　證明密碼協(xié)議的正確性與安全性的理論和方法通�？梢苑譃閮纱箢�(lèi)：形式化方法和計(jì)算復(fù)雜性方法。形式化方法可使協(xié)議設(shè)計(jì)者通過(guò)系統(tǒng)分析將注意力專(zhuān)注于接口、系統(tǒng)環(huán)境假設(shè)、系統(tǒng)在不同條件下的狀態(tài)、條件不滿(mǎn)足時(shí)系統(tǒng)出現(xiàn)的（異常）情況以及系統(tǒng)不變量等，并通過(guò)系統(tǒng)驗(yàn)證為協(xié)議提供必要的安全保證；而計(jì)算復(fù)雜性方法通常又被稱(chēng)為可證明安全性方法，它基于一些最基礎(chǔ)的假設(shè)或公理（例如，假設(shè)單向函數(shù)存在，或某些計(jì)算問(wèn)題的困難性等），采用規(guī)約的方法，將協(xié)議的安全目標(biāo)規(guī)約到一個(gè)己知或公認(rèn)的困難問(wèn)題。關(guān)于這兩種方法的詳細(xì)介紹，請(qǐng)參見(jiàn)相關(guān)文獻(xiàn)。

　　計(jì)算復(fù)雜性方法采用了演繹推理方法（例如，從某個(gè)已知的假設(shè)推出一個(gè)結(jié)論的邏輯過(guò)程），其重點(diǎn)則放在攻破協(xié)議到某個(gè)公認(rèn)為困難問(wèn)題的可證明規(guī)約。其中，隨機(jī)預(yù)言機(jī)模型（rom）就是這樣一種應(yīng)用最廣泛的成功模型，基于rom模型的理論和方法也被稱(chēng)為可證明安全理論。可證明安全理論和技術(shù)始于20世紀(jì)80年代初期，最初用于分析加密方案和簽名方案的安全性，后來(lái)則用于分析密碼協(xié)議的安全性。使用可證明安全性理論來(lái)證明協(xié)議的安全性主要包括以下5個(gè)主要過(guò)程：

　　（1）模型描述：

　�。�2）該模型內(nèi)安全目標(biāo)定義；

　�。�3）安全假設(shè)說(shuō)明；

　�。�4）協(xié)議描述；

　�。�5）協(xié)議在該安全模型內(nèi)達(dá)到其安全目標(biāo)的證明。

　　1． 一種rfid協(xié)議攻擊者模型

　　目前，使用上述兩種方法專(zhuān)門(mén)來(lái)研究rfid協(xié)議安全性的公開(kāi)成果幾乎沒(méi)有。本節(jié)僅討論使用可證明安全性理論和方法來(lái)證明和分析reid協(xié)議的一些思考，主要討論模型描述以及該模型內(nèi)的安全目標(biāo)定義（可證明安全性理論中最為關(guān)鍵的部分之一）。首先討論一下rπd系統(tǒng)環(huán)境下的攻擊者模型。一個(gè)rfid系統(tǒng)是由多個(gè)主體和通信信道構(gòu)成的。對(duì)rfid協(xié)議進(jìn)行安全性分析時(shí)，通常將后臺(tái)數(shù)據(jù)庫(kù)和讀寫(xiě)器當(dāng)作同一個(gè)獨(dú)立和唯一的通信實(shí)體來(lái)對(duì)待。這種處理方法符合大多數(shù)rfid系統(tǒng)通信信道安全假設(shè)。鑒于前向信道與反向信道的不對(duì)稱(chēng)性（如圖所示），對(duì)它們分別進(jìn)行處理。這樣，攻擊者所能獲得的信息僅來(lái)自于rfid系統(tǒng)的信道，如圖所示。在該模型中，所有實(shí)體的通信都在攻擊者的控制下，攻擊者可以任意地讀取、插入、刪除、篡改、延遲發(fā)送、重放任何消息，也可以在任何時(shí)候發(fā)起與任何實(shí)體的任意應(yīng)答。

　　圖 reid系統(tǒng)信道模型用

　　下面用oracle查詢(xún)來(lái)模型化攻擊者的能力。用t表示標(biāo)簽，用r表示讀寫(xiě)器，兩者參與的rfid協(xié)議為p。協(xié)議雙方都可以發(fā)起p的多個(gè)實(shí)例，用πⁱ_t表示第i個(gè)標(biāo)簽實(shí)例，用πⁱ_t表示第j個(gè)讀寫(xiě)器實(shí)例。攻擊者可以進(jìn)行如下oracle查詢(xún)。

　　query（πⁱ_t，m1，m3）：該查詢(xún)刻畫(huà)了攻擊者通過(guò)前向信道向t發(fā)送消息m1，并在接收到t的應(yīng)答后再向t發(fā)送消息m3。

　　send（πⁱ_t，m2）：該查詢(xún)刻畫(huà)了攻擊者通過(guò)反向信道向r發(fā)送消息m2，并接收r的應(yīng)答。

　　execute（πⁱ_t，πⁱ_r）：該查詢(xún)刻畫(huà)了攻擊者執(zhí)行t和r的協(xié)議p的一個(gè)實(shí)例，并獲得通過(guò)前向信道和反向信道交換的所有消息。

　　execute*（πⁱ_t，πⁱ_r）：該查詢(xún)刻畫(huà)了攻擊者執(zhí)行t和r的協(xié)議p的一個(gè)實(shí)例，但是攻擊者僅能獲得通過(guò)前向信道交換的所有消息。

　　corrupt（πⁱ_t，sk）：該查詢(xún)刻畫(huà)了攻擊者收買(mǎi)t的能力，使t泄漏自己私有存儲(chǔ)空間內(nèi)的密鑰信息，并可能會(huì)使用攻擊者提供的密鑰信息sk來(lái)代替原t存儲(chǔ)區(qū)中的內(nèi)容（依據(jù)使用的算法和場(chǎng)景的不同，可能是共享密鑰或者公鑰）。

　　2． 安全目標(biāo)定義

　　令t∈{q，s，e，e*，c}，其中q、s、e、e*、c分別表示上述幾種oracle查詢(xún)。攻擊者與目標(biāo)t以及可能的r進(jìn)行一定的交互過(guò)程之后，獲得一個(gè)交互記錄ω（t）。攻擊者的攻擊目的是要區(qū)分t）和t2，以便確認(rèn)出所攻擊的目標(biāo)。此時(shí)，攻擊者也可以分別與t；和t2再次進(jìn)行交互過(guò)程，并可以獲得兩個(gè)交互記錄ω1（t）和ω2（t）。此時(shí)，給定協(xié)議p，攻擊者的優(yōu)勢(shì)定義為：

　　advp（）＝2pr［t1＝t2］－1