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

張 興，韓 冬，馬曉光

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

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

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

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

1 邏輯推理分析法

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

表1 邏輯推理分析法的對比表

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

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

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

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

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

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

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

2 模型模擬檢測法

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

表2 模型模擬檢測法的對比表

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

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

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

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

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

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

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

3 定理歸納證明法

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

表3 定理歸納證明法的對比表

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

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

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

4 其他衍生驗證法

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

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

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

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

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

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

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

7)基于Horn 擴展邏輯的非否認建模與驗證方法是基于Horn 邏輯擴展模型驗證非否認協(xié)議的驗證方法。本方法主要強調(diào)驗證非否認協(xié)議的非否認性和公平性，并對協(xié)議的非否認性和公平性建模。在對協(xié)議的建模過程中還需要對協(xié)議的誠實主體、惡意主體、仲裁進行建模，提出了適用于非否認協(xié)議的驗證算法?；贖orn 邏輯擴展的模型可應(yīng)用于無窮會話交疊運行的情況，提高了對協(xié)議保密性的驗證效率。

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

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

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

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

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

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

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

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

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

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

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

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

6 總結(jié)與展望

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

表4 各類安全協(xié)議驗證方法對比表

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

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

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

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

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

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

［4］高尚等. 安全協(xié)議形式化分析研究［J］.密碼學報.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］薛海峰，荊立夏.認證協(xié)議的必要條件證明［J］.計算機工程，2011，37(11):144－145.

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

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

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

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

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

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

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

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

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

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

［25］陳莉.一種新的安全協(xié)議驗證邏輯及其串空間語義［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/.