安全協(xié)議的形式化分析技術(shù)方法研究

付浩

摘要：安全協(xié)議是解決網(wǎng)絡(luò)安全問題最有效的手段之一。然而，由于互聯(lián)網(wǎng)的開放性和協(xié)議的并發(fā)性，安全協(xié)議的設(shè)計(jì)和分析一直是一個(gè)復(fù)雜而困難的問題。實(shí)踐證明，借助形式化的方法或工具分析安全協(xié)議是非常必要而且行之有效的。安全協(xié)議的形式化分析已有三十多年的歷史，一直存在兩類不同的方法：計(jì)算方法和符號(hào)方法。符號(hào)方法用形式化語言和符號(hào)推理對(duì)協(xié)議進(jìn)行分析和驗(yàn)證，更容易實(shí)現(xiàn)自動(dòng)化分析。但是由于對(duì)密碼學(xué)原語和攻擊者能力的理想建模，使得這類分析方法的肯定性結(jié)論往往并不直接具有現(xiàn)實(shí)意義，被認(rèn)為沒有真正建立起密碼學(xué)的可靠性。

關(guān)鍵詞：安全協(xié)議；符號(hào)方法；計(jì)算方法

隨著信息技術(shù)和網(wǎng)絡(luò)技術(shù)的飛速發(fā)展，互聯(lián)網(wǎng)的廣泛應(yīng)用已成為社會(huì)進(jìn)步和發(fā)展的重要標(biāo)志之一。然而，由于網(wǎng)絡(luò)的開放性，它給人們的生活帶來極大方便的同時(shí)也帶來了許多安全隱患。安全協(xié)議是解決網(wǎng)絡(luò)安全問題最有效的手段之一，安全協(xié)議的正確實(shí)施對(duì)于保障網(wǎng)絡(luò)虛擬世界中各種組織和系統(tǒng)、各種商務(wù)和交易的安全運(yùn)行起著十分關(guān)鍵的作用。安全協(xié)議”（也稱密碼協(xié)議）是建立在密碼體制基礎(chǔ)上的一種通信協(xié)議，它運(yùn)行在計(jì)算機(jī)網(wǎng)絡(luò)或分布式系統(tǒng)中，借助于密碼算法為實(shí)現(xiàn)密鑰分配、身份認(rèn)證、電子商務(wù)交易等任務(wù)的各方約定一系列執(zhí)行步驟和執(zhí)行規(guī)則。

由于安全協(xié)議中各消息之間存在著復(fù)雜的相互作用和制約關(guān)系，許多設(shè)計(jì)并投入實(shí)際應(yīng)用的安全協(xié)議在運(yùn)行時(shí)不一定能夠真正實(shí)現(xiàn)它所聲明的安全性質(zhì)。據(jù)英國(guó)學(xué)者Gavin Lowet估計(jì)，在已公開發(fā)表的安全協(xié)議中，有超過一半的安全協(xié)議實(shí)際上不能實(shí)現(xiàn)它所聲明的安全性質(zhì)。造成安全協(xié)議失敗的原因主要在于：1）協(xié)議設(shè)計(jì)者對(duì)安全陸需求（目標(biāo)）的定義和刻畫不完全、或理解上有偏差；2）協(xié)議分析者對(duì)設(shè)計(jì)出來的安全協(xié)議是否滿足安全性需求缺乏足夠的、全面的安全性分析。

自20世紀(jì)70年代末以來，安全協(xié)議的分析已經(jīng)成為一個(gè)研究熱點(diǎn)。但是，由于安全協(xié)議設(shè)計(jì)與分析的復(fù)雜性，使得該研究變得十分困難并具有挑戰(zhàn)性。安全協(xié)議的分析方法主要有兩大類：攻擊檢驗(yàn)方法和形式化分析方法。攻擊檢驗(yàn)方法根據(jù)已知的各種攻擊方法對(duì)協(xié)議進(jìn)行攻擊測(cè)試，以攻擊是否有效來檢驗(yàn)協(xié)議是否安全。

自上世紀(jì)八十年代開始使用形式化方法對(duì)安全協(xié)議進(jìn)行分析以來，安全協(xié)議的形式化分析就存在兩類截然不同的方法：計(jì)算方法和符號(hào)方法。這兩類方法都是通過對(duì)安全協(xié)議的執(zhí)行過程和攻擊者能力建立數(shù)學(xué)模型，以及對(duì)安全協(xié)議的安全性需求給出形式化定義，實(shí)現(xiàn)對(duì)協(xié)議安全陸的嚴(yán)格證明。

計(jì)算方法（也稱可證明安全方法）一般是在計(jì)算復(fù)雜性理論框架下的一種“歸約”方法，將對(duì)安全方案或者協(xié)議的攻擊有效變換到對(duì)大整數(shù)分解和離散對(duì)數(shù)等困難問題的求解，其結(jié)果更具密碼學(xué)可靠性。在計(jì)算方法的協(xié)議建模中，安全協(xié)議執(zhí)行時(shí)產(chǎn)生的消息是二進(jìn)制位串，各種密碼學(xué)原語是一個(gè)多項(xiàng)式時(shí)間算法，而攻擊者（也稱敵手）是一個(gè)關(guān)于安全參數(shù)多項(xiàng)式時(shí)間計(jì)算的圖靈機(jī)。協(xié)議的安全性通過概率和計(jì)算復(fù)雜度表示，即攻擊者不能經(jīng)常且輕易地做一些壞事情。計(jì)算方法以其復(fù)雜的定義和定理強(qiáng)化了密碼學(xué)基礎(chǔ)，對(duì)設(shè)計(jì)和研究某些協(xié)議起了很重要的作用。但是，也正由于這些特點(diǎn)使得其證明較復(fù)雜，不容易驗(yàn)證。對(duì)具體協(xié)議的分析與論證往往需要發(fā)現(xiàn)較特殊的證明途徑，很多細(xì)節(jié)難以很好把握，基本上都是手工證明，導(dǎo)致即使分析中等規(guī)模的安全協(xié)議，其證明也耗時(shí)較長(zhǎng)且容易出錯(cuò)。

符號(hào)方法（也稱Dolev-Yao方法）用形式化語言和符號(hào)推理進(jìn)行協(xié)議分析和驗(yàn)證，更便于對(duì)協(xié)議的自動(dòng)化分析。在符號(hào)方法的協(xié)議建模中，消息都是形式化的符號(hào)表達(dá)式，各種密碼學(xué)原語的理想安全屬性通過對(duì)這些表達(dá)式應(yīng)用各種符號(hào)操作得到，這些符號(hào)操作像一個(gè)黑盒，而不是基于二進(jìn)制位串的具體密碼學(xué)算法。符號(hào)方法通常以Dolev-Yao模型或擴(kuò)充的Dolev-Yao模型作為安全協(xié)議攻擊者模型，攻擊者只能對(duì)符號(hào)表達(dá)式施行一些給定的符號(hào)操作，但沒有計(jì)算時(shí)間限制。符號(hào)方法具有自然而強(qiáng)有力的密碼學(xué)直覺，近年已用于許多協(xié)議的設(shè)計(jì)和分析，并肯定一些現(xiàn)有協(xié)議的安全性以及發(fā)現(xiàn)很多協(xié)議的攻擊。但是，基于高度抽象的符號(hào)形式特征往往不能準(zhǔn)確地表達(dá)協(xié)議的安全性質(zhì)，因此這類分析方法的肯定性結(jié)論未必具有現(xiàn)實(shí)意義（即使符號(hào)分析方法斷言一個(gè)協(xié)議是“安全”的，其未必在現(xiàn)實(shí)中是安全的）或密碼學(xué)可靠性。

綜上所述，表1給出了計(jì)算方法和符號(hào)方法的比較。現(xiàn)在普遍的認(rèn)識(shí)是：基于計(jì)算復(fù)雜性的計(jì)算方法是（密碼學(xué)）可靠的，但是證明過程是高度創(chuàng)造性的手工數(shù)學(xué)式證明，這對(duì)于目前越來越復(fù)雜的安全協(xié)議，不僅證明本身越來越復(fù)雜，而且證明的正確性也越來越不容易；而大多數(shù)建立于Dolve-Yao模型之上的符號(hào)方法借助于符號(hào)演繹體系的演算機(jī)制，證明過程容易實(shí)現(xiàn)自動(dòng)化，但是由于對(duì)密碼學(xué)原語和攻擊者能力的理想建模，使得某些類型的肯定性結(jié)論往往并不直接具有現(xiàn)實(shí)意義，被認(rèn)為沒有真正建立起密碼學(xué)的可靠性。

通過為安全協(xié)議的符號(hào)方法建立更精確的計(jì)算密碼學(xué)語義，對(duì)密碼學(xué)原語的實(shí)現(xiàn)提出明確要求，還可以證實(shí)或改善協(xié)議的形式化證明與該協(xié)議具體實(shí)例之間的關(guān)聯(lián)。

計(jì)算方法，也稱可證明安全方法，本質(zhì)上是一種“歸約”方法：首先形式化的定義安全方案或協(xié)議的安全目標(biāo)；然后根據(jù)攻擊者的能力構(gòu)建一個(gè)形式化的攻擊者模型，嚴(yán)格定義攻擊者所掌握的攻擊手段和資源；最后通過安全性證明指出，如果存在攻破某個(gè)安全方案或協(xié)議的攻擊者，那么我們可以使用這個(gè)攻擊者作為子程序來構(gòu)造解決某個(gè)已知計(jì)算難題的有效算法。由于我們相信某些計(jì)算難題的有效算法是不存在的，因此我們得到結(jié)論：不存在攻擊者能夠以不可忽略的概率攻破該安全方案或協(xié)議。