智能化電視網(wǎng)絡(luò)安全協(xié)議的驗(yàn)證方法綜述

張 興，韓 冬，馬曉光

(1.遼寧工業(yè)大學(xué) 電子與信息工程學(xué)院，遼寧 錦州 121001;2.北京歌華有線電視網(wǎng)絡(luò)股份有限公司，北京100000)

隨著互聯(lián)網(wǎng)產(chǎn)業(yè)的發(fā)展，電視技術(shù)的雙向化、智能化趨勢(shì)逐步凸顯。當(dāng)前我國(guó)智能化電視的普及率已達(dá)到23.2%，根據(jù)格蘭研究數(shù)據(jù)，截至到2013 年三季度末，我國(guó)有線電視雙向網(wǎng)絡(luò)覆蓋用戶為8 914.3 萬(wàn)戶，有線電視雙向網(wǎng)絡(luò)滲透用戶為2 641.1 萬(wàn)戶。預(yù)計(jì)2015 年全國(guó)縣級(jí)以上城市有線廣播電視網(wǎng)絡(luò)80%以上基本實(shí)現(xiàn)雙向化。用戶可以實(shí)現(xiàn)在雙向電視機(jī)頂盒端生活繳費(fèi)、網(wǎng)上購(gòu)物、網(wǎng)銀管理等一系列家庭事務(wù)，極大地方便了用戶的生活，然而也正是由于雙向交互式機(jī)頂盒、智能電視的功能越來越豐富，各種信息也越來越多地被收集到數(shù)字電視網(wǎng)絡(luò)中，如果缺乏有效的協(xié)議安全性意味著數(shù)字電視網(wǎng)絡(luò)中的信息將存在著巨大的安全隱患。2013年11 月LG 智能電視被曝會(huì)強(qiáng)制收集用戶的瀏覽記錄、觀看歷史等個(gè)人信息，并通過HTTP 流量加密傳輸?shù)紾B.smartshare.legtvsdp.com，被制造商用來投放廣告。2014 年5 月哥倫比亞大學(xué)有關(guān)專家公布紅色按鈕攻擊漏洞，利用該漏洞可以攻擊采用HbbTV 標(biāo)準(zhǔn)的智能電視。2014 年8 月溫州地區(qū)部分電視用戶機(jī)頂盒遭黑客攻擊，電視畫面遭到非法入侵，嚴(yán)重地影響了用戶的正常生活［1－2］。這種情形的出現(xiàn)無(wú)疑是電視網(wǎng)絡(luò)的通信安全機(jī)制不夠完善所導(dǎo)致的合法用戶的現(xiàn)實(shí)生活受到影響。通信協(xié)議的驗(yàn)證機(jī)制是確保電視網(wǎng)絡(luò)安全的主要手段之一，通過安全協(xié)議的驗(yàn)證法［3－4］選擇安全性更高的通信協(xié)議就顯得極為重要。通常安全協(xié)議主要由消息交換規(guī)則和加密手段兩部分組成。由于在安全協(xié)議的設(shè)計(jì)過程中存在著安全目標(biāo)的微妙性、運(yùn)行環(huán)境的復(fù)雜性、攻擊者的不定性以及協(xié)議本身的高并發(fā)性等因素，使得協(xié)議本身存在著一些缺陷。因而，正確的選擇一種適合的驗(yàn)證方法來驗(yàn)證安全協(xié)議的的可用性、正確性、安全性是很必要的。安全協(xié)議的形式化分析思想最早是在1978 年由Needham 和Schroeder 兩人共同提出，但真正意義上的協(xié)議驗(yàn)證思想是由Dolev 和Yao 二人提出的Dolev－Yao 模型［5］。當(dāng)Dolev－Yao 模型提出后，一部分研究者對(duì)其進(jìn)行了進(jìn)一步研究和擴(kuò)展，相關(guān)的協(xié)議分析工具也被研發(fā)出來，如Interrogator［6］、NRL 協(xié)議分析器［7］等。1989 年，Burrows、Abadi 和Needham 三人提出了BAN 邏輯［8］，BAN 邏輯具有簡(jiǎn)單直觀、推理思路清晰等特點(diǎn)。使安全協(xié)議形式化分析領(lǐng)域的可操作性變得簡(jiǎn)潔，推動(dòng)了協(xié)議驗(yàn)證的進(jìn)一步發(fā)展。然而BAN 邏輯的缺陷也是不容忽視的，如抽象假設(shè)過度、不能對(duì)新鮮性建模等。對(duì)于BAN 邏輯的缺陷研究者們對(duì)其作了改進(jìn)，提出了GNY 邏輯［9］、AT 邏輯［10］、SVO 邏輯［11］等BAN 邏輯的改進(jìn)形式。20 世紀(jì)90 年代中期，當(dāng)Lowe 利用通信順序進(jìn)程對(duì)協(xié)議進(jìn)行分析時(shí)，得出了更清晰的驗(yàn)證結(jié)果。CSP 驗(yàn)證模型便廣泛地應(yīng)用于協(xié)議驗(yàn)證分析領(lǐng)域。到90 年代末期，由Fabrega、Herzog 和Guttma 提出的串空間模型［12］及Paulson 歸納法［13］，引領(lǐng)了應(yīng)用定理歸納證明法對(duì)安全協(xié)議驗(yàn)證分析的新局面。

隨著安全協(xié)議驗(yàn)證領(lǐng)域的不斷發(fā)展，近五年提出的一些衍生類協(xié)議驗(yàn)證方法正在引領(lǐng)著協(xié)議驗(yàn)證分析領(lǐng)域的新潮流，如綁定項(xiàng)證明法［14］、軟件模擬法［15］、SPVT 驗(yàn)證工具［16］、理性安全協(xié)議推理系統(tǒng)［17］、改進(jìn)的BAN 邏輯［18］、改進(jìn)型有色Petri 網(wǎng)的協(xié)議驗(yàn)證法［19］、基于Horn 擴(kuò)展邏輯的非否認(rèn)建模與驗(yàn)證方法［20］、基于SAT 的安全協(xié)議惰性形式化分析方法［21］、串空間的改進(jìn)方法IVAP［22］、含時(shí)間因素的安全協(xié)議形式化分析方法［23］、混合的安全協(xié)議分析法［24］、新的協(xié)議驗(yàn)證邏輯［25］等。這些安全協(xié)議著重于對(duì)經(jīng)典的協(xié)議驗(yàn)證方法的改進(jìn)、擴(kuò)展或提出了新的通信協(xié)議驗(yàn)證方法。但在安全協(xié)議形式化分析領(lǐng)域，每一類驗(yàn)證方法都存在著相應(yīng)的缺陷或不足。因此，對(duì)于這些改進(jìn)或新提出的安全協(xié)議進(jìn)行總結(jié)、分析，并在此基礎(chǔ)上指出新的研究方向顯得十分必要。

下面，本文就以下幾類安全協(xié)議驗(yàn)證方法做詳細(xì)介紹。

1 邏輯推理分析法

邏輯推理分析法指的是在協(xié)議的驗(yàn)證過程中，通過將協(xié)議描述為對(duì)應(yīng)驗(yàn)證規(guī)則的語(yǔ)法，對(duì)相應(yīng)變量進(jìn)行假設(shè)，在符合假設(shè)和約定規(guī)則的前提下，進(jìn)行邏輯推導(dǎo)驗(yàn)證協(xié)議是否達(dá)到了預(yù)期目的的驗(yàn)證方法，邏輯推理分析法的對(duì)比如表1 所示。

表1 邏輯推理分析法的對(duì)比表

1)BAN 邏輯是由Michael Burrows，Martin Abadi 等提出的，它是協(xié)議形式化分析的工具之一。BAN 邏輯是一種基于主體信念來從已知的信念中推出新的信念的邏輯規(guī)則。通過應(yīng)用BAN 邏輯來驗(yàn)證協(xié)議從信息傳遞過程中是否可以推出最終運(yùn)行的結(jié)果。BAN 邏輯的應(yīng)用過程:將協(xié)議的條件進(jìn)行合理的假設(shè)，通過假設(shè)來構(gòu)造BAN 邏輯中的公式，然后將這些公式應(yīng)用BAN 邏輯的語(yǔ)法進(jìn)行推理，最終得出驗(yàn)證結(jié)果。

2)GNY 邏輯于1990 年由Gong，Needham 和Yahalom 提出。屬于類BAN 邏輯的擴(kuò)展，相較于BAN 邏輯對(duì)邏輯分析能力、可識(shí)別概念、判斷規(guī)則等方面進(jìn)行了改進(jìn)。GNY 邏輯總共44 條規(guī)則，推導(dǎo)過程較為復(fù)雜。

3)AT 邏輯是由Abadi M 和Tuttle M R 提出的。AT 邏輯較BAN 邏輯而言，重新形式化了BAN 邏輯，采用將信仰作為源綁定形式和可作廢的知識(shí)對(duì)待，具備了更好的自然邏輯語(yǔ)義模型和合理的計(jì)算模型。

4)SVO 邏輯是由Syverson 和Van Oorschot 提出，SVO 邏輯吸取BAN、GNY、AT 等邏輯的優(yōu)勢(shì)，建立自己簡(jiǎn)潔合理的推理模型，在形式化語(yǔ)義方面，SVO 邏輯取消了AT 邏輯中的部分限制，重新定義了部分概念。當(dāng)前SVO 邏輯被主要用于電子商務(wù)中相關(guān)協(xié)議的研究。

5)Kailar 邏輯［26］的提出主要是為了電子商務(wù)協(xié)議的可追究性，以解決主體向第三方證明另一方執(zhí)行的責(zé)任行為。然而它缺乏對(duì)簽名密文的分析能力，證明協(xié)議時(shí)不夠嚴(yán)格。

6)CS 邏輯［27］由Coffey 和Saidha 提出，它結(jié)合了謂詞邏輯和模態(tài)邏輯的特點(diǎn)，也是一種將時(shí)間和邏輯結(jié)構(gòu)相結(jié)合的邏輯。但CS 邏輯對(duì)環(huán)境因素考慮不足，在某些特定環(huán)境下不能對(duì)協(xié)議進(jìn)行有效驗(yàn)證。

7)KG 邏輯［28］由Kailar 和Gligor 提出的，來驗(yàn)證雙方的最終信仰，即驗(yàn)證雙方互相發(fā)送和接收?qǐng)?bào)文能否從最初的信仰發(fā)展成協(xié)議要達(dá)到的最終目的。通過驗(yàn)證協(xié)議運(yùn)行中的信仰變換來檢測(cè)協(xié)議中是否存在著缺陷。

2 模型模擬檢測(cè)法

模型模擬檢測(cè)法指的是采用模擬工具或構(gòu)建模型的方式，將初始狀態(tài)下的協(xié)議進(jìn)行檢測(cè)，通過對(duì)協(xié)議運(yùn)行開始到運(yùn)行結(jié)束的路徑進(jìn)行檢測(cè)，判斷是否協(xié)議存在缺陷的驗(yàn)證方法。模型模擬檢測(cè)法具有高度自動(dòng)化的特點(diǎn)，模型模擬檢測(cè)法則對(duì)比見表2。

表2 模型模擬檢測(cè)法的對(duì)比表

1)有限狀態(tài)機(jī)FSM［29］是一種應(yīng)用于系統(tǒng)動(dòng)態(tài)行為的建模，借助狀態(tài)圖進(jìn)行可視化表示。通過對(duì)有限狀態(tài)機(jī)的不斷的研究，可以被用于更多更復(fù)雜行為的建模。但FSM 的實(shí)現(xiàn)也存在著復(fù)用性差，維護(hù)困難等問題。

2)Dolev－Yao 模型是由Dolev 和Yao 最早提出，經(jīng)過后來研究者T Genet 和F Klay［30］等的進(jìn)一步擴(kuò)展。Dolev－Yao 模型首先對(duì)安全協(xié)議進(jìn)行層次劃分，將安全算法和協(xié)議本身區(qū)分研究，然后對(duì)協(xié)議的正確性、安全性等進(jìn)行研究。提出了重視攻擊者知識(shí)和能力的原則。

3)CSP 方法［31］即通信順序進(jìn)程方法，由C.A.R.Hoare提出。他將輸入、輸出作為程序語(yǔ)言的基本要素，將實(shí)現(xiàn)順序進(jìn)程間通信的并行組合。對(duì)安全協(xié)議進(jìn)行驗(yàn)證時(shí)首先從協(xié)議說明中建立模型，再結(jié)合FDR 工具(故障偏差精煉檢測(cè)器)［32］檢測(cè)協(xié)議是否存在問題。

4)Spin 模擬檢測(cè)方法［33］是由貝爾實(shí)驗(yàn)室的形式化小組研發(fā)的協(xié)議檢測(cè)模型，使用Promela 語(yǔ)言建模，整個(gè)系統(tǒng)可以看作是擴(kuò)展的有限狀態(tài)機(jī)。主要用于對(duì)于線性時(shí)態(tài)邏輯的正確性檢測(cè)。

5)murφ 模型檢測(cè)法［34］由J.C. Mitchell，M.Mitchell 和Stern 最早應(yīng)用于對(duì)協(xié)議預(yù)期性質(zhì)的建模，通過加入入侵者模型，在應(yīng)用狀態(tài)枚舉法來檢測(cè)系統(tǒng)狀態(tài)都符合規(guī)范。

6)Interrogator 由Millen 等人提出的，基于狀態(tài)機(jī)技術(shù)的協(xié)議分析器。Interrogator 對(duì)協(xié)議分析時(shí)采取前向搜索，從初始狀態(tài)直到最終狀態(tài)存在不安全路徑。

7)NRL 模型檢測(cè)工具由Meadows 等人研發(fā)，它是Dolev－Yao 模型的擴(kuò)充版本。NRL 工具采取后向搜索方式，從協(xié)議執(zhí)行的最終狀態(tài)出發(fā)搜尋是否存在到達(dá)初始狀態(tài)的路徑。

3 定理歸納證明法

定理歸納證明法是通過將協(xié)議形式化的模型和規(guī)則進(jìn)行驗(yàn)證，在協(xié)議的模型中是否滿足了初始的規(guī)則。定理歸納證明法相較模型模擬檢測(cè)法是從協(xié)議的正方向驗(yàn)證，直接對(duì)協(xié)議的規(guī)約進(jìn)行證明。定理歸納證明法對(duì)比如表3 所示。

表3 定理歸納證明法的對(duì)比表

1)串空間模型(strand space model)由Thayer 和Herzog 等人提出的形式化方法。主要用于安全協(xié)議的認(rèn)證性和私密性的驗(yàn)證。卿斯?jié)h等針對(duì)此方法的不足進(jìn)行了擴(kuò)展，并提出了擴(kuò)展后的通用串空間模型。隨著對(duì)串空間方法的不斷研究，串空間與信任管理相結(jié)合，使得串空間模型更好地應(yīng)用于多種安全協(xié)議的驗(yàn)證。

2)Paulson 歸納法由L C Paulson 提出，這種方法通過將協(xié)議歸納定義為所有時(shí)間可能路徑的集合。一條路徑即為一個(gè)包含多輪協(xié)議的通信事件序列。可以模擬所有攻擊及密鑰丟失事，通過對(duì)路徑歸納來證明屬性安全。

3)重寫逼近法(Rewriting Approximation Method)［35］由Boichut Y 等人提出。此方法的驗(yàn)證目標(biāo)是驗(yàn)證協(xié)議中不存在任何攻擊。在實(shí)際協(xié)議驗(yàn)證中，重寫逼近法對(duì)協(xié)議的安全屬性進(jìn)行正面驗(yàn)證，較其他測(cè)試方法而言具有更好的可靠性。

4 其他衍生驗(yàn)證法

其他衍生驗(yàn)證法指的是通過研究一些經(jīng)典協(xié)議的驗(yàn)證方法，對(duì)這些協(xié)議驗(yàn)證方法進(jìn)行擴(kuò)展，或者選取新的驗(yàn)證角度，構(gòu)建出全新的協(xié)議驗(yàn)證模型。

1)綁定項(xiàng)證明法指的是由微觀角度通過形式化理論來判定協(xié)議的綁定項(xiàng)(即加密項(xiàng))的完備性。驗(yàn)證過程中若存在綁定項(xiàng)不符合規(guī)則，可認(rèn)定協(xié)議存在缺陷，快速準(zhǔn)確地給予判定協(xié)議結(jié)果。

2)軟件模擬法是指利用軟件模型模擬出協(xié)議運(yùn)行環(huán)境，從而對(duì)安全協(xié)議進(jìn)行驗(yàn)證。針對(duì)RFID 安全協(xié)議而言，利用Linux 系統(tǒng)、gcc 編譯器、Mysql 數(shù)據(jù)庫(kù)相結(jié)合模擬出RFID 系統(tǒng)，在將協(xié)議導(dǎo)入模擬系統(tǒng)中運(yùn)行，最終得出驗(yàn)證結(jié)果。

3)SPVT 驗(yàn)證工具是基于Objective Caml 開發(fā)的協(xié)議驗(yàn)證工具。利用類π 演算來描述安全協(xié)議。SPVT 驗(yàn)證工具根據(jù)邏輯程序的不動(dòng)點(diǎn)計(jì)算驗(yàn)證安全性質(zhì)，來驗(yàn)證出不滿足安全性質(zhì)的缺陷。

4)理性安全協(xié)議推理系統(tǒng)是基于博弈邏輯ATL 和ATEL的擴(kuò)展研究，針對(duì)理性環(huán)境下，在傳統(tǒng)博弈邏輯的基礎(chǔ)下，提出了新的推理系統(tǒng)rA－TEL－A。在此推理系統(tǒng)中，將協(xié)議進(jìn)行形式化描述，并對(duì)協(xié)議進(jìn)行模擬驗(yàn)證。

5)改進(jìn)的BAN 邏輯是根據(jù)BAN 邏輯在對(duì)協(xié)議驗(yàn)證過程中存在的一些缺陷，而對(duì)其進(jìn)行改進(jìn)的協(xié)議驗(yàn)證邏輯。在使用BAN 邏輯驗(yàn)證協(xié)議的過程中，BAN 邏輯的初始假設(shè)、消息形式化描述轉(zhuǎn)換、邏輯語(yǔ)義、推理規(guī)則及探測(cè)協(xié)議存在的攻擊等幾方面存在不足。通過對(duì)這方面分析及改進(jìn)，改進(jìn)的BAN邏輯又從消息形式化描述、消息含義推理規(guī)則、先行判斷規(guī)則這三個(gè)角度對(duì)改進(jìn)的BAN 邏輯進(jìn)行了驗(yàn)證，提高了BAN 邏輯驗(yàn)證的安全可靠性。

6)改進(jìn)型有色Petri 網(wǎng)的協(xié)議驗(yàn)證法通過對(duì)傳統(tǒng)有色Petri 的分析改進(jìn)而提出的。運(yùn)用傳統(tǒng)有色Petri 網(wǎng)安全協(xié)議分析法對(duì)協(xié)議進(jìn)行驗(yàn)證，主要通過倒推的方法即在檢測(cè)前確定出可能的不安全狀態(tài)，驗(yàn)證此不安全狀態(tài)可達(dá)，從而分析協(xié)議可能的缺陷，但對(duì)于未知的不安全狀態(tài)無(wú)法進(jìn)行檢測(cè)。另外，對(duì)于驗(yàn)證入侵者的協(xié)議時(shí)，構(gòu)造協(xié)議模型時(shí)由于對(duì)入侵者的攻擊步驟不了解，使其狀態(tài)規(guī)模快速增長(zhǎng)，導(dǎo)致空間爆炸的問題。然而改進(jìn)型有色Petri 網(wǎng)在對(duì)協(xié)議進(jìn)行分析驗(yàn)證時(shí)，不必了解未知的安全狀態(tài)，只需要了解一個(gè)攻擊成功的目標(biāo)。改進(jìn)型有色Petri 網(wǎng)對(duì)攻擊成功的知識(shí)集與可以獲取的知識(shí)集進(jìn)行整合，將其融入到傳統(tǒng)的有色Petri 網(wǎng)中縮小入侵攻擊步驟的范圍，緩解了傳統(tǒng)有色Petri 網(wǎng)在驗(yàn)證協(xié)議時(shí)所引起的空間爆炸問題。

7)基于Horn 擴(kuò)展邏輯的非否認(rèn)建模與驗(yàn)證方法是基于Horn 邏輯擴(kuò)展模型驗(yàn)證非否認(rèn)協(xié)議的驗(yàn)證方法。本方法主要強(qiáng)調(diào)驗(yàn)證非否認(rèn)協(xié)議的非否認(rèn)性和公平性，并對(duì)協(xié)議的非否認(rèn)性和公平性建模。在對(duì)協(xié)議的建模過程中還需要對(duì)協(xié)議的誠(chéng)實(shí)主體、惡意主體、仲裁進(jìn)行建模，提出了適用于非否認(rèn)協(xié)議的驗(yàn)證算法。基于Horn 邏輯擴(kuò)展的模型可應(yīng)用于無(wú)窮會(huì)話交疊運(yùn)行的情況，提高了對(duì)協(xié)議保密性的驗(yàn)證效率。

8)基于SAT 的安全協(xié)議惰性形式化分析方法是一種基于SAT 問題的協(xié)議分析方法。加入惰性思想優(yōu)化初始狀態(tài)和轉(zhuǎn)換規(guī)則，根據(jù)協(xié)議的復(fù)雜度自動(dòng)調(diào)用命題公式的范式形式，提升了模型的驗(yàn)證效率。其次根據(jù)在消息類型上定義的偏序關(guān)系，本方法可以檢測(cè)到更多類型的缺陷攻擊。

9)串空間的改進(jìn)方法IVAP 是一種以串空間為理論基礎(chǔ)，根據(jù)認(rèn)證協(xié)議的一致性屬性及測(cè)試分量唯一性屬性而建立的安全性驗(yàn)證算法。本方法證明了安全協(xié)議的安全性，而且能運(yùn)用改進(jìn)協(xié)議生成算法為有漏洞的協(xié)議生成安全的改進(jìn)協(xié)議。但本方法不能實(shí)現(xiàn)對(duì)無(wú)線認(rèn)證協(xié)議的安全屬性驗(yàn)證。

10)含時(shí)間因素的安全協(xié)議形式化分析方法是一種針對(duì)包含時(shí)間因素的有色Petri 網(wǎng)形式化分析法。本方法利用有色Petri 網(wǎng)中內(nèi)置的全局自動(dòng)時(shí)鐘標(biāo)記，并通過仿真和生成狀態(tài)圖的方式對(duì)時(shí)間相關(guān)性質(zhì)進(jìn)行驗(yàn)證。由于利用系統(tǒng)的內(nèi)置自動(dòng)時(shí)鐘，在建模及驗(yàn)證過程中，系統(tǒng)提供時(shí)鐘支持方法，因此對(duì)于一些復(fù)雜的包時(shí)間因素的安全協(xié)議，此方法依然可以清晰的描述驗(yàn)證。

11)混合的安全協(xié)議分析法是以SPALL 邏輯為基礎(chǔ)，結(jié)合了可證安全的思想，提出概率推導(dǎo)的分析方法。本方法將形式化證明中的模態(tài)邏輯分析法和可證明安全法兩者相結(jié)合，將邏輯假設(shè)的成立概率結(jié)合到協(xié)議的推導(dǎo)過程中，形成一種概率推導(dǎo)方法。根據(jù)概率的條件，來判別協(xié)議假設(shè)安全與否，從而確定協(xié)議整體的安全性。此方法克服了兩種方法的各自缺陷，具有簡(jiǎn)單易用、分析全面的特點(diǎn)。

12)新的協(xié)議驗(yàn)證邏輯是一種可以驗(yàn)證安全協(xié)議的認(rèn)證性、非否認(rèn)性、公平性等特性的邏輯方法。本方法提出了新的邏輯構(gòu)件、推理規(guī)則及公理。通過增加Hash 函數(shù)的密碼原語(yǔ)相關(guān)的邏輯謂詞、推理規(guī)則和公理，實(shí)現(xiàn)了對(duì)基于對(duì)稱密鑰體制、公鑰密碼體制和Hash 函數(shù)密碼體制協(xié)議的分析驗(yàn)證能力。并通過串空間語(yǔ)義對(duì)新邏輯進(jìn)行驗(yàn)證，證明了此邏輯方法具備了邏輯驗(yàn)證的正確性。

13)基于SPIN 的安全自適應(yīng)協(xié)議棧的形式化驗(yàn)證法［36］屬于一種自動(dòng)化的模型檢測(cè)方法。本方法將相鄰搜索機(jī)制和路由協(xié)議作為切入點(diǎn)，對(duì)安全協(xié)議進(jìn)行自動(dòng)檢測(cè)、分析并指出存在缺陷。因此本驗(yàn)證法具備自動(dòng)化程度高、缺陷自動(dòng)檢測(cè)等優(yōu)點(diǎn)，但是在對(duì)協(xié)議建模的過程中需要采集各方面的約定規(guī)則、抽象假設(shè)，導(dǎo)致在構(gòu)建協(xié)議的premola 描述模型時(shí)較為復(fù)雜。

14)變異性監(jiān)測(cè)(Veriability)驗(yàn)證法［37］是一種針對(duì)密碼協(xié)議進(jìn)行自動(dòng)化驗(yàn)證的方法。本方法主要應(yīng)用于電子選舉協(xié)議，可以對(duì)匿名認(rèn)證用戶的加密信息進(jìn)行檢測(cè)，同時(shí)對(duì)于部署廣泛的加密協(xié)議可以自動(dòng)評(píng)估檢測(cè)，發(fā)現(xiàn)其不安全的漏洞。本驗(yàn)證法具備部分自動(dòng)化、驗(yàn)證安全屬性較為全面，但由于僅僅針對(duì)電子投票協(xié)議的驗(yàn)證，所以此方法存在驗(yàn)證的局限性。

15)一種自動(dòng)化的模型檢測(cè)方法［38］是集合了模型提取和代碼生成于一體的驗(yàn)證方法。本方法通過代買編寫、模型抽取的方式來自動(dòng)構(gòu)建協(xié)議的驗(yàn)證模型，同時(shí)盡可能編譯出真實(shí)的協(xié)議環(huán)境，達(dá)到更精確的驗(yàn)證。本方法具有自動(dòng)化程度高、驗(yàn)證精確度高等優(yōu)點(diǎn)，然而對(duì)于代碼的編譯過程較為復(fù)雜，構(gòu)建出的模型具有針對(duì)性，所以驗(yàn)證角度有限。

16)協(xié)議代碼模塊化驗(yàn)證方法［39］是一種基于聲明和執(zhí)行不變論密碼學(xué)的應(yīng)用方法，本方法開發(fā)了加密嵌入邏輯模型的庫(kù)結(jié)構(gòu)，并提出了一個(gè)驗(yàn)證理論，證明了模塊化代碼驗(yàn)證的合理性。同時(shí)本方法具備驗(yàn)證結(jié)果精確度高、可擴(kuò)展性強(qiáng)的優(yōu)點(diǎn)，但對(duì)于驗(yàn)證角度而言僅針對(duì)協(xié)議中的加密代碼模塊進(jìn)行驗(yàn)證。

17)基于拍處理的自動(dòng)化驗(yàn)證方法［40］屬于自動(dòng)化模型檢測(cè)的驗(yàn)證法。本方法應(yīng)用了關(guān)于概率的時(shí)間演算的加密算法，以此更好地對(duì)協(xié)議的實(shí)時(shí)性、概率性、加密性等幾方面進(jìn)行驗(yàn)證。本方法具備自動(dòng)化程度高、驗(yàn)證精確性高的優(yōu)點(diǎn)，但其驗(yàn)證存在局限性，而且不能對(duì)外部攻擊者進(jìn)行追蹤檢測(cè)。

5 協(xié)議驗(yàn)證法的比較

針對(duì)以上的安全協(xié)議驗(yàn)證方法，分析對(duì)比各類驗(yàn)證方法的優(yōu)缺點(diǎn)，如表4 所示。對(duì)各類驗(yàn)證方法的特點(diǎn)進(jìn)行比較，總結(jié)出每類驗(yàn)證方法適合驗(yàn)證的安全協(xié)議。邏輯推理分析法雖然簡(jiǎn)單直觀、可視化，但其由于過度抽象化等原因只適用于驗(yàn)證規(guī)模較小、特定的小系統(tǒng)的安全協(xié)議;模型模擬檢測(cè)法具備自動(dòng)化程度高、協(xié)議自動(dòng)校正等優(yōu)勢(shì)，但不能很好地克服空間控制及主題數(shù)目限制的問題，根據(jù)其這些特點(diǎn)適用于模型適中、較大系統(tǒng)的安全協(xié)議;定理歸納證明法雖然自動(dòng)化程度不高、部分證明復(fù)雜，但由于其語(yǔ)義清晰、分析直觀、避免了空間控制問題等特點(diǎn)，所以其適用于不受模型限制、大型系統(tǒng)的安全協(xié)議;其他衍生驗(yàn)證法是前幾類安全協(xié)議驗(yàn)證法的延伸，通過對(duì)一些經(jīng)典的的驗(yàn)證方法進(jìn)行了改進(jìn)及擴(kuò)展，并加以創(chuàng)新，推動(dòng)了安全協(xié)議驗(yàn)證領(lǐng)域不斷發(fā)展，這一類安全協(xié)議驗(yàn)證方法適用于驗(yàn)證更為廣泛的安全協(xié)議。

6 總結(jié)與展望

當(dāng)前，隨著有線電視網(wǎng)絡(luò)承載的應(yīng)用量越來越多，其安全性必須得到保障。因此，驗(yàn)證電視網(wǎng)絡(luò)通信協(xié)議的驗(yàn)證方法的研究就顯得極為重要。協(xié)議驗(yàn)證法是從確定協(xié)議系統(tǒng)與其運(yùn)行環(huán)境的界面、協(xié)議行為的描述、協(xié)議特性的定義及證明協(xié)議符合規(guī)定語(yǔ)義等角度對(duì)協(xié)議的安全性進(jìn)行分析驗(yàn)證。然而以上的協(xié)議驗(yàn)證方法雖然經(jīng)過不斷的研究擴(kuò)展具備了各自的特點(diǎn)，但每類協(xié)議驗(yàn)證法都或多或少存在著一些不足。為了研究出一種更加簡(jiǎn)潔、通用、自動(dòng)化程度高的協(xié)議驗(yàn)證方法，還需要做進(jìn)一步的努力。針對(duì)當(dāng)前的安全協(xié)議驗(yàn)證領(lǐng)域提出如下的研究方向:

表4 各類安全協(xié)議驗(yàn)證方法對(duì)比表

1)對(duì)于邏輯角度證明，降低形式化抽象的“完美假設(shè)”。對(duì)于應(yīng)用邏輯推理法來對(duì)安全協(xié)議進(jìn)行驗(yàn)證時(shí)，首先要對(duì)安全協(xié)議的運(yùn)行環(huán)境、理論條件作出假設(shè)，然而這些假設(shè)或多或少存在著缺陷，如過度理想化、條件完整化等。這些過于完美的初始假設(shè)已然使協(xié)議的精確驗(yàn)證出現(xiàn)了部分偏差，因此在對(duì)安全協(xié)議進(jìn)行初始假設(shè)的過程中，盡量將抽象假設(shè)的理想程度降低，以此提高對(duì)協(xié)議驗(yàn)證的準(zhǔn)確性。

2)將自動(dòng)化驗(yàn)證理念進(jìn)一步擴(kuò)展，以適應(yīng)更廣泛的安全協(xié)議。對(duì)于安全協(xié)議驗(yàn)證領(lǐng)域而言，若驗(yàn)證工具可以自動(dòng)的對(duì)安全協(xié)議進(jìn)行查找漏洞、缺陷修復(fù)、構(gòu)建修正協(xié)議，那么將極大地提高安全協(xié)議的驗(yàn)證效率。在安全協(xié)議驗(yàn)證領(lǐng)域中，模型模擬檢測(cè)法在自動(dòng)化驗(yàn)證方面較其他協(xié)議驗(yàn)證方法具有著很大的優(yōu)勢(shì)，但此方法也存在著不容忽視的缺陷。因此如何改進(jìn)模型模擬檢測(cè)法的缺陷或者提高其他驗(yàn)證方法的自動(dòng)化程度將值得對(duì)此進(jìn)行進(jìn)一步研究。

3)嘗試將幾類協(xié)議驗(yàn)證法進(jìn)行結(jié)合，優(yōu)勢(shì)互補(bǔ)，推出一種驗(yàn)證性能優(yōu)越的協(xié)議驗(yàn)證法。安全協(xié)議驗(yàn)證方法的類型如上文所述，每一種安全協(xié)議驗(yàn)證方法都有著自己的優(yōu)勢(shì)和不足。若用某一類驗(yàn)證方法對(duì)安全協(xié)議進(jìn)行驗(yàn)證，那么得出的驗(yàn)證結(jié)果并不能完全確定所驗(yàn)證協(xié)議是否是安全的、正確的、可行的。因此如何將幾類安全協(xié)議驗(yàn)證法進(jìn)行結(jié)合，使得結(jié)合后的驗(yàn)證方法具備了這幾種驗(yàn)證法的優(yōu)勢(shì)，同時(shí)彌補(bǔ)這幾種驗(yàn)證法的不足，最終得出的協(xié)議驗(yàn)證方法可以對(duì)安全協(xié)議進(jìn)行更加可靠、更加全面的驗(yàn)證。這種將驗(yàn)證法相結(jié)合的研究方向勢(shì)必成為通信協(xié)議驗(yàn)證領(lǐng)域研究的新趨勢(shì)。

［1］蔡盛勇，吳靜.基于SSL 協(xié)議的智能電視安全支付方案［J］.電視技術(shù)，2013，37(24):49－51.

［2］《電視技術(shù)》編輯部.信息安全:風(fēng)高浪急［J］.電視技術(shù)，2014，38(20):1.

［3］馮登國(guó)，范紅.安全協(xié)議形式化分析理論與方法研究綜述［J］.中國(guó)科學(xué)院研究生院學(xué)報(bào)，2003，20(4):389–406.

［4］高尚等. 安全協(xié)議形式化分析研究［J］.密碼學(xué)報(bào).2014，1(5):504－512.

［5］DOLEV D，YAO A.On the security of public key protocols［J］.IEEE Trans.Information Theory，1983，29(2):98－208.

［6］MILLEN J K，CLARK S C，F(xiàn)REEDAM S B.The interrogator:protocol security analysis［J］.TSE，1987，13(2):274－288.

［7］MEADOWS C.The NRL protocol analyzer:anoverview［J］.Journal of k c Progranarning，1996，26(2):113－131.

［8］BURROES M，ABADI M，NEEDHAM R. A logic of authentication［J］.ACM Transaction in Computer Systems，1990，8(1):18－36.

［9］GONG L，NEEDHAM R，YAHALOM R.Reasoning about belief in cryptographic protocols［C］//Proc.1990 IEEE Symp. Security and Privacy.［S.l.］:IEEE Press，1990:234－248.

［10］ABADI M，TUTTLE M R.A semantics for a logic of authentication［C］//Proc.10th Annual ACM Symposium on Principles of Distributed Computing.［S.l.］:ACM Press，1991:201－216.

［11］SYVERSON P F，OORSCHOT P C.A unified cryptographic protocol logic［R］.Washington D.C:Naval research lab，1996.

［12］THAYER F J，HERZOG J C，GUTTMAN J D.Strand spaces:why is a security protocol correct［C］//Proc.1998 IEEE Symposium on Security and Privacy.［S.l.］:IEEE Press，1998:160－171.

［13］PAULSON L C.Proving properties of security protocols［C］//Proc.IEEE Computer Security Foundations Workshop X.［S.l.］:IEEE Press，1997:70－83.

［14］薛海峰，荊立夏.認(rèn)證協(xié)議的必要條件證明［J］.計(jì)算機(jī)工程，2011，37(11):144－145.

［15］郭艾俠，李峰，熊俊濤.RFID 認(rèn)證協(xié)議的研究及仿真［J］.實(shí)驗(yàn)室研究與探索，2010，29(3):61－65.

［16］李夢(mèng)君，李舟軍，陳火旺.SPVT:一個(gè)有效的安全協(xié)議驗(yàn)證工具［J］.軟件學(xué)報(bào)，2006(4):898－906.

［17］劉海，彭長(zhǎng)根，任祉靜.一種理性安全協(xié)議形式化分析方法及應(yīng)用［J］.貴州大學(xué)學(xué)報(bào):自然科學(xué)版，2014，31(6):77－84.

［18］王正才，許道云，王曉峰，等. BAN 邏輯的可靠性分析與改進(jìn)［J］.計(jì)算機(jī)工程，2012，38(17):110－115.

［19］張卉，李續(xù)武，趙媛莉，等.改進(jìn)型有色Petri 網(wǎng)的安全協(xié)議分析［J］.計(jì)算機(jī)工程與科學(xué)，2013(7):60－63.

［20］徐暢，李舟軍，郭華，等. 基于Horn 擴(kuò)展邏輯的非否認(rèn)協(xié)議建模與驗(yàn)證［J］.清華大學(xué)學(xué)報(bào)，2012，52(10):1488－1495.

［21］顧純祥，王煥孝，鄭永輝，等.基于SAT 的安全協(xié)議惰性形式化分析方法［J］.通信學(xué)報(bào)，2014，35(11):117－125.

［22］張孝紅，李謝華.基于串空間的安全協(xié)議自動(dòng)化驗(yàn)證算法［J］.計(jì)算機(jī)工程，2011，37(5):131－133.

［23］范玉濤，蘇桂平.一種含時(shí)間因素的安全協(xié)議形式化分析方法［J］.計(jì)算機(jī)應(yīng)用與軟件，2013，30(1):315－318.

［24］霍騰飛，李益發(fā)，鄧帆.一種混合的安全協(xié)議分析方法［J］.計(jì)算機(jī)應(yīng)用與軟件，2011，28(3):289－292.

［25］陳莉.一種新的安全協(xié)議驗(yàn)證邏輯及其串空間語(yǔ)義［J］.計(jì)算機(jī)工程，2011，37(1):145－148.

［26］DUTERTRE B，SCHNEIDER S. Using a PVS embedding of CSP to verify authentication rotocols［M］.［S.l.］:Springer Berlin Heidelberg，1997.

［27］COFFEY T，SAIDHA P.Logic for verifying public－key cryptographic protocols［J］.IEEE Proc. Computers and Digital Techniques，1997，144(1):28－32.

［28］BOLDYREVA A.KUMAR V.Extended abstract provab le－security analysis of authenticated encryption in kerberos［C］//Proc. IEEE Symmposium on Security and Privacy.New York:IEEE Press，2007:92－100.

［29］JAMES R，IVAR J，GRADY B.The Unified modeling language reference manual［M］.Boston:Addison Wesley，1999.

［30］GENET T，KLAY F.Rewriting for cryptographic protocol verification［C］//Proc.17th International Conference on Automated Deduction.Pittsburgh:IEEE Press，2000:9－9.

［31］HOARE C A R.Communicating sequential processes［J］.Prentice－Hall International，1985，31(1):413－443.

［32］LOWE G.Breaking and fixing the needham－schroeder public－key protocol using FDR［C］//Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg:Springer Berlin，1996:147－166.

［33］GNESI S，LENZINI G，LATELLA D，et al. An automatic SPIN validation of a safety critical railway control system［C］//Proc.2000 IEEE Intemational Conference on Dependable Systems and Networks.Piscataway:IEEE Press，2000:119－124.

［34］MITCHELL J C，MITCHELL M，STERN U.Automated analysis of crypto－graphic protocols using mur［C］//Proc.1997 IEEE Symposium on Security and Privacy. New York:IEEE Press，1997:141－151.

［35］BOICHUT Y，GENET T，JENSEN T，et al. Rewriting approximations for fast prototyping of static analyzers［M］.［S.l.］:Springer Berlin Heidelberg，2007:48–62.

［36］RIPON S，Mahbub S，INTIAZ－UD－DIN K M［J］.International Journal of Engineering and Technology，2013:254－256.

［37］SMYTH B.Formal verification of cryptographic protocols with automated reasoning［D］.Birmingham:University of Birmingham，2011.

［38］AVALLE M，PIRONTI A，RICCARDO S. Formal verification of security protocol implementations:a survey［J］.Formal Aspects of Computing，2014，26(1):99－123.

［39］Gordon. Modular verification of security protocol code by typing［J］.Acm Sigplan Notices，2010，45(1):445－456.

［40］TA V，BUTTYáN L，DVIR A. On formal and automatic security verification of WSN transport protocols［EB/OL］.［2014－12－31］.http://www.hindawi.com/journals/isrn/2014/891467/.