智能化電視網絡安全協議的驗證方法綜述

張 興，韓 冬，馬曉光

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

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

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

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

1 邏輯推理分析法

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

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

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

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

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

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

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

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

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

2 模型模擬檢測法

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

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

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

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

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

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

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

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

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

3 定理歸納證明法

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

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

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

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

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

4 其他衍生驗證法

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 協議驗證法的比較

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

6 總結與展望

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

表4 各類安全協議驗證方法對比表

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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