基于形式化方法的安全協(xié)議安全性分析*

鄧 輝，張寶峰，劉 暉，毛軍捷，畢海英

(中國信息安全測評中心,北京，100085)

基于形式化方法的安全協(xié)議安全性分析*

鄧 輝，張寶峰，劉 暉，毛軍捷，畢海英

(中國信息安全測評中心,北京，100085)

協(xié)議安全是確保網(wǎng)絡(luò)數(shù)據(jù)安全的基礎(chǔ)。傳統(tǒng)的基于觀察的人工分析協(xié)議安全性分析已不能滿足安全需求。如何研究安全協(xié)議及安全屬性的性質(zhì)，使兩者在統(tǒng)一框架下實(shí)現(xiàn)可分析和驗(yàn)證是亟待解決的問題，形式化分析為解決這一問題提供了精確的數(shù)學(xué)手段和強(qiáng)大的分析工具。對已有的安全協(xié)議形式化分析方法進(jìn)行了歸納和總結(jié)，并從等價驗(yàn)證、協(xié)議優(yōu)化和增強(qiáng)分析準(zhǔn)確度三方面提出了未來的研究設(shè)想。

安全協(xié)議;安全性分析;形式化方法;網(wǎng)絡(luò)安全

0 引 言

互聯(lián)網(wǎng)自誕生以來，就以驚人的速度在全世界迅速發(fā)展?；ヂ?lián)網(wǎng)在人類社會及生活中的廣泛引入，加快了社會信息的交互，使得現(xiàn)實(shí)世界中的各種系統(tǒng)均對應(yīng)出現(xiàn)在互聯(lián)網(wǎng)這個虛擬系統(tǒng)中。遺憾的是，互聯(lián)網(wǎng)自身的開放性、共享性以及不穩(wěn)定性引發(fā)了眾多網(wǎng)絡(luò)安全問題。近年來攻擊者利用安全協(xié)議漏洞，偽裝成合法的通信者竊聽、更改或者重放信息，引發(fā)網(wǎng)絡(luò)安全事件的現(xiàn)象層出不窮。

為確保數(shù)據(jù)通信安全，在眾多安全協(xié)議中，有一類特殊的協(xié)議旨在實(shí)現(xiàn)不安全信道上的數(shù)據(jù)傳輸安全，稱為安全協(xié)議。安全協(xié)議是一種運(yùn)用密碼技術(shù)解決網(wǎng)絡(luò)安全問題的有效方式，在不可靠通信環(huán)境下，基于加密算法，通過加密信息交換實(shí)現(xiàn)保密性、完整性、認(rèn)證性以及不可抵賴性。

自1976年Hellman等人提出第一個安全協(xié)議Needham-Schroeder后[1]，各種類型的安全協(xié)議例如SSL[2]、IPSec[3]、S/MIME[4]和SHITP[5]等陸續(xù)推出，并被廣泛應(yīng)用于身份認(rèn)證和密鑰分配等多個領(lǐng)域。目前，安全協(xié)議已成為構(gòu)建高安全性網(wǎng)絡(luò)的基礎(chǔ)。根據(jù)實(shí)現(xiàn)目標(biāo)的不同，安全協(xié)議可分為密碼交換協(xié)議、認(rèn)證協(xié)議、認(rèn)證密鑰交換協(xié)議、電子商務(wù)協(xié)議和安全多方計(jì)算協(xié)議。

安全協(xié)議旨在實(shí)現(xiàn)通信安全。但是，事實(shí)上一部分安全協(xié)議在出現(xiàn)之初被認(rèn)為是安全的，卻在很短時間內(nèi)被證明是非安全的。如著名的Needham-Schroeder協(xié)議在推出三年后被證明存在安全缺陷。據(jù)統(tǒng)計(jì)，已公開的安全協(xié)議中有超過一半的協(xié)議不能實(shí)現(xiàn)所聲稱的安全性。大部分安全協(xié)議非安全的原因不在于所采用的加密機(jī)制，而在于在設(shè)計(jì)過程中存在漏洞，即設(shè)計(jì)過程中忽略了協(xié)議被攻擊的可能性。

目前針對安全協(xié)議安全性的分析方法主要有兩類：攻擊檢驗(yàn)和形式化分析。但是僅能窮舉已知攻擊方法對協(xié)議進(jìn)行攻擊測試的攻擊檢驗(yàn)法不能全面評估安全協(xié)議安全性。形式化作為全面分析目標(biāo)對象行為及結(jié)構(gòu)分析的有利方法，可形式化建模安全協(xié)議及安全屬性，將安全性分析轉(zhuǎn)化為安全協(xié)議的形式化模型是否滿足安全屬性對應(yīng)的形式化模型的過程，此過程避免了攻擊檢驗(yàn)方法的局限性，有利于發(fā)現(xiàn)安全協(xié)議的未知攻擊。自九十年代以來，此方法已成為安全協(xié)議分析領(lǐng)域的熱點(diǎn)。

形式化方法在安全協(xié)議的安全性分析中的共同技術(shù)思想是通過建立形式化建模規(guī)則，將安全協(xié)議的某個或者某些特征進(jìn)行形式化規(guī)范，最終利用數(shù)學(xué)方法實(shí)現(xiàn)其正確性或者非正確性推導(dǎo)。實(shí)踐證明形式化方法在安全協(xié)議的安全性分析中發(fā)揮了很好作用。

1 已有的協(xié)議安全性形式化分析方法

安全協(xié)議形式化分析研究起源于1983年Dolev和Yao提出的完美密碼假設(shè)以及Dolev-Yao模型[6]，在假設(shè)密碼算法不存在任何安全問題的前提下，給出安全協(xié)議的攻擊者模型，并依此討論安全協(xié)議安全屬性是否得到滿足，此理論成為安全協(xié)議形式化分析方法的基本框架。目前，已有的安全協(xié)議安全性形式化分析主要從認(rèn)知邏輯、模型檢查、定理證明三個角度出發(fā)得以實(shí)現(xiàn)。

1.1 基于模態(tài)邏輯的推理方法

基于模態(tài)邏輯的推理方法是安全協(xié)議形式化分析中使用最廣泛的方法，突出代表是基于知識和信仰的邏輯——BAN邏輯。此邏輯在1989年提出[7]，被應(yīng)用于Needham-Schroeder、Kerberos等部分著名協(xié)議的安全性分析，并且發(fā)現(xiàn)部分已知和未知漏洞。

BAN邏輯是最早用于驗(yàn)證認(rèn)證協(xié)議和密鑰交換協(xié)議的形式化方法，其處理流程如圖1所示，包括安全協(xié)議理想化，即將協(xié)議形式化描述為一組BAN邏輯公式；協(xié)議初始假設(shè)確定，確定安全協(xié)議正確運(yùn)行的初始假設(shè)條件；協(xié)議邏輯推理，將BAN邏輯公式與初始假設(shè)條件合并進(jìn)行邏輯推演，得到安全協(xié)議運(yùn)行的最終結(jié)果；協(xié)議安全性分析，判斷最終結(jié)果是否達(dá)到安全協(xié)議的設(shè)計(jì)目標(biāo)。如果結(jié)果與目標(biāo)相符，則安全協(xié)議安全性得到滿足，否則即安全協(xié)議存在漏洞。

圖1 基于模態(tài)邏輯的安全協(xié)議安全性分析框架

但是，BAN邏輯實(shí)現(xiàn)安全協(xié)議安全性分析過程中，安全協(xié)議理想化與初始假設(shè)確定均存在模糊處理，導(dǎo)致最終的安全分析結(jié)果在精確度上無法完全保證。為此，研究學(xué)者對BAN邏輯進(jìn)行了不同程度的改造，推出了類BAN邏輯系統(tǒng)[8-10]，其中包括：GNY邏輯、AT邏輯、CS邏輯和KG邏輯等。類BAN邏輯在一定程度上緩解了BAN邏輯的局限性，但是并未完全解決問題。

目前仍沒有一種BAN類邏輯能夠完全解決BAN邏輯的所有缺陷。

1.2 基于模型的狀態(tài)檢驗(yàn)方法

模型檢查由Clarke、Emerson等人在1981年提出。基于此研究，用于安全協(xié)議分析的模型檢測工具陸續(xù)得到開發(fā)，如Brutus模型檢測器、SMV系統(tǒng)、Interrogator工具、NRL協(xié)議分析器等?；谀Ｐ偷臓顟B(tài)檢驗(yàn)方法基于自動化工具實(shí)現(xiàn)自動執(zhí)行，并能在系統(tǒng)不滿足性質(zhì)時提供反例路徑，因此在工業(yè)界備受推崇[11-16]。

模型檢查在安全協(xié)議安全性分析過程中的引入，目的在于擴(kuò)展自動驗(yàn)證技術(shù)的應(yīng)用領(lǐng)域，同時基于其自身具有形式化方法的優(yōu)勢最終精確化安全協(xié)議分析的結(jié)果。

利用模型檢查進(jìn)行安全協(xié)議安全性分析的技術(shù)思路描述如圖2所示。此圖表示將安全協(xié)議形式化為一個四元組，包括狀態(tài)集合、狀態(tài)轉(zhuǎn)移集合、狀態(tài)轉(zhuǎn)移規(guī)則、狀態(tài)轉(zhuǎn)移過程。通過前向搜索或者后向搜索判斷協(xié)議是否安全。其中：

(1)前向搜索：從某個初始狀態(tài)出發(fā)，看協(xié)議運(yùn)行過程中是否會到達(dá)不安全狀態(tài)；

(2)后向搜索：確定一個不安全狀態(tài)，看是否存在一個達(dá)到合法狀態(tài)的通路；

圖2 基于模型檢查的安全協(xié)議安全性分析框架

模型檢查在協(xié)議安全分析中體現(xiàn)出一定的技術(shù)優(yōu)勢，主要包括：自動化程度高，以批處理的方式可一次性檢驗(yàn)安全協(xié)議的多條路徑；TOE安全性質(zhì)采用邏輯公式書寫，精確度高；當(dāng)規(guī)約不被滿足時，會生成一條反例路徑，作為診斷信息，幫助設(shè)計(jì)者及時修正TOE錯誤。

但是模型檢查在檢測安全性的過程中需要窮舉安全協(xié)議對應(yīng)模型中所有可能的可達(dá)狀態(tài)，可能會產(chǎn)生狀態(tài)空間爆炸，由此，模型檢查對于無窮狀態(tài)空間問題不可判定。同時，模型檢查處理的對象同樣是TOE模型而非TOE本身，形式化過程存在模糊處理。因此，分析過程可能存在偏差，導(dǎo)致分析結(jié)果存在誤報(bào)。

1.3 基于定理證明的安全目標(biāo)驗(yàn)證方法

定理證明源自人工智能發(fā)展時期A.Newell等人編制出的稱為邏輯理論機(jī)的數(shù)學(xué)定理證明程序?；诖?，Abadi和Gordon利用 Spi演算刻畫協(xié)議并運(yùn)行，并利用Dolev-Yao完美加密假設(shè)和觀測等價實(shí)現(xiàn)安全協(xié)議分析[17]。之后，F(xiàn)abrega等人提出利用串空間模型描述協(xié)議合法主體的行為及攻擊者的動作序列，通過分析串連接情況判斷協(xié)議安全屬性是否得到滿足[18]。為實(shí)現(xiàn)基于串空間模型分析方法的自動化，工具Athena已經(jīng)得到實(shí)現(xiàn)。但是Athena無法保證搜索過程一定終止，且需限制協(xié)議運(yùn)行主體的數(shù)量[19]。

除此以外，歸納法[20]、秩函數(shù)[21]等陸續(xù)被用于實(shí)現(xiàn)安全協(xié)議特定安全屬性的證明。但是，這些方法均難以完全自動化。

定理證明技術(shù)在協(xié)議安全性分析中的基本原理可描述如圖3所示，即將安全協(xié)議描述為代數(shù)或邏輯公式，聯(lián)合假定必要的公理集，證明安全性質(zhì)對應(yīng)的待證定理集。

從分析的角度看，與模型檢查不同的是，定理證明是判斷安全協(xié)議是否滿足安全需求，此過程實(shí)施的是安全協(xié)議的正面分析；而模型檢查是尋找安全協(xié)議可能面臨的威脅有哪些，此過程實(shí)施的是安全協(xié)議的反面分析。

圖3 基于定理證明的安全協(xié)議安全性分析框架

相比于其他安全分析技術(shù)，定理證明誤報(bào)率很低，是眾多靜態(tài)分析方法中最準(zhǔn)確的方法。此方法可以處理無限狀態(tài)空間問題。

但是定理證明需要形式化描述安全協(xié)議的前置條件、后置條件以及循環(huán)不變量，此過程效率較低，較難用于復(fù)雜安全協(xié)議的驗(yàn)證。同時，把安全協(xié)議及其安全屬性形式化轉(zhuǎn)換為代數(shù)或者邏輯公式時相關(guān)特征信息存在遺漏的可能，一旦缺乏則可能導(dǎo)致證明結(jié)果的不精確性。

2 已有分析方法的比較

在安全協(xié)議安全性分析過程中，形式化方法相比攻擊檢驗(yàn)而言，其優(yōu)點(diǎn)比較突出，即可以避免攻擊檢驗(yàn)中需要進(jìn)行狀態(tài)窮舉而造成測試子集選取的不完備性。

不同的方法在安全協(xié)議安全性分析過程中的相同點(diǎn)和不同點(diǎn)，可從分析方法的目的、原理、是否可處理無限狀態(tài)、以及分析角度來進(jìn)行說明，具體描述如表1所示。

表1 已有的安全協(xié)議安全性形式化分析方法

3 已有分析方法面臨的問題

3.1 無法有效刻畫網(wǎng)絡(luò)協(xié)議

已有的分析方法無論是從設(shè)計(jì)、實(shí)現(xiàn)，還是其他階段，對網(wǎng)絡(luò)協(xié)議利用如BAN 邏輯、串空間、Spi演算，還是更一般化的形式化方法進(jìn)行刻劃，都會或多或少地?fù)p失一些有用的屬性信息，從而導(dǎo)致分析方法的有效性和可靠性被打了折扣。

3.2 優(yōu)化理論未引入

已有的安全協(xié)議形式化分析方法均直接對安全協(xié)議本身或協(xié)議對應(yīng)的形式化模型進(jìn)行處理，并未進(jìn)行任何優(yōu)化處理，分析過程中容易出現(xiàn)“狀態(tài)爆炸”現(xiàn)象。安全協(xié)議自身的優(yōu)化實(shí)現(xiàn)對于優(yōu)化安全協(xié)議安全性分析，提高分析效率具有實(shí)際的意義。

3.3 其他問題

基于模態(tài)邏輯的推理方法、基于模型的狀態(tài)檢驗(yàn)方法及基于定理證明的安全目標(biāo)驗(yàn)證方法可用于判斷網(wǎng)絡(luò)協(xié)議是否滿足不同的安全需求。但是，它們無法實(shí)現(xiàn)無限狀態(tài)空間網(wǎng)絡(luò)協(xié)議形式化分析、不安全狀態(tài)定位、最大化分析不安全狀態(tài)等中的部分問題是目前網(wǎng)絡(luò)協(xié)議形式化分析需要解決的重點(diǎn)問題。

4 安全協(xié)議安全性形式化分析的未來

面對已有安全協(xié)議安全性形式化分析存在的不足，未來應(yīng)重點(diǎn)關(guān)注以下三個方面的研究。

4.1 實(shí)現(xiàn)分級等價驗(yàn)證

等價驗(yàn)證的產(chǎn)生源于對門級電路設(shè)計(jì)過程中功能的一致性檢測。目前，通過調(diào)研發(fā)現(xiàn)等價驗(yàn)證已經(jīng)在并發(fā)系統(tǒng)的行為功能性驗(yàn)證、行為及結(jié)構(gòu)一致性檢測、行為及結(jié)構(gòu)優(yōu)化工作中得到了初步的研究并取得了一定的處理效果。

基于等價驗(yàn)證的一致性思想，可以被用于實(shí)現(xiàn)安全協(xié)議與安全性質(zhì)的匹配驗(yàn)證，基本思路可設(shè)計(jì)為從攻擊者的角度，如果不能區(qū)分安全協(xié)議與安全性質(zhì)所對應(yīng)的形式化模型觀測等價，則表明安全性質(zhì)得到滿足。

整體的技術(shù)思路如圖4所示。

圖4 基于等價驗(yàn)證的安全協(xié)議安全性分析框架

提取基于等價驗(yàn)證的安全協(xié)議安全性分析特征后，表1可更新如表2所示。

表2 安全協(xié)議安全性形式化分析方法

通過分析表2，可以了解到等價驗(yàn)證在已有方法中優(yōu)勢較為明顯，因此未來應(yīng)加大這方面的研究。但是如何選擇合適的等價關(guān)系是需要思考的問題。如果將協(xié)議看作為所有可能事件路徑的集合，則不同協(xié)議對應(yīng)的事件路徑集合不同。因此，協(xié)議等價關(guān)系應(yīng)該從協(xié)議運(yùn)行規(guī)則的角度出發(fā)分別構(gòu)建低級別的外部等價及高級別的內(nèi)部等價關(guān)系。

4.2 實(shí)現(xiàn)協(xié)議優(yōu)化

在安全協(xié)議以及安全性質(zhì)的形式化建模過程中，涉及諸多規(guī)則的說明、約束和生成，導(dǎo)致最終獲得的形式化模型通常比較復(fù)雜，因此在自動化處理中往往耗時較多，效率低下導(dǎo)致形式化方法在大規(guī)模工程應(yīng)用中無法推廣。未來需要研究形式化模型的優(yōu)化方法，提高形式化方法的整體處理效率。同時，由于形式化模型的優(yōu)化，對于減緩“狀態(tài)爆炸”也會起到促進(jìn)的作用。

4.3 提高分析準(zhǔn)確度

形式化的過程是一個高度提煉和抽象目標(biāo)特征的過程，會使安全協(xié)議以及安全性質(zhì)分別與它們的形式化模型之間存在一定的誤差，造成某些信息的丟失，對最終安全性分析結(jié)果的準(zhǔn)確性造成或多或少的損失。未來需要優(yōu)化形式化方法應(yīng)用于安全協(xié)議安全性分析時涉及的模型轉(zhuǎn)換規(guī)則，最終提高分析結(jié)果的準(zhǔn)確性。

5 結(jié) 語

已有的安全協(xié)議形式化分析方法為網(wǎng)絡(luò)協(xié)議的通用分析提供了一種新的途徑。但是，通過本文的分析，發(fā)現(xiàn)已有分析方法在不同方面存在不同程度的問題，且尚未形成完整的理論體系，難以解決網(wǎng)絡(luò)協(xié)議設(shè)計(jì)和驗(yàn)證領(lǐng)域中的許多關(guān)鍵問題。未來需進(jìn)一步開展協(xié)議的通用形式化分析方法研究，對于促進(jìn)網(wǎng)絡(luò)通信安全具有重要的理論意義。

[1] Blanchet B. Security Protocol Verification: Symbolic and Computational Models [C]. Proceedings of the First International Conference on Principles of Security and Trust. 2012:3-29.

[2] Krawczyk H, Paterson K G, Wee H. On the Security of the TLS Protocol: A Systematic Analysis [J]. Advances in Cryptology-Crypto 2013. 2013:429-448.

[3] Singh G, Dhanda S K. Performance Analysis of Security Schemes in Wireless Sensor Network[J]. International Journal of Advanced Research in Computer and Communication Engineering. 2013, 2(8): 3217-3223.

[4] Lauter K. The Advantages of Elliptic Curve Cryptography for Wireless Security [J]. IEEE Wireless Communications. 2004, 11(1): 62-67.

[5] Martin F J, Plaza E, Rodríguez-Aguilar J A. An Infrastructure for Agent-based Systems: An Interagent Approach [J]. International Journal of Intelligent Systems. 2000, 15(3): 217-240.

[6] Dolev D, YAO A. On the Security for Public key Protocols [J]. IEEE Transaction on Information Theory. 1983, 29(2): 198-208.

[7] Meadows C A. Formal Verification of Cryptographic Protocols: A Survey [J], Springer Berlin Heidelberg. 1995.

[8] Gritzalis S, Spinellis D,Georgiadis P. Security Protocols Over Open Networks and Distributed Systems: Formal Methods for Their Analysis, Design, and Verification[J]. Computer Communications. 1999,22(8):697-709.

[9] Agray N, Van Der Hoek W, De Vink E. On BAN Logics for Industrial Security Protocols [J]. Springer Berlin Heidelberg. 2002:29-36.

[10] YUAN J J. An Enhanced Two-Factor User Authentication in Wireless Sensor Networks [J]. Telecommunication Systems.2014,55(1): 105-113.

[11] Lowe G. Breaking and Fixing the Needham-Schroder Pubic-key Protocol Using FDR[J]. In Tools and Algorithms for the Construction and Analysis of Systems. 1996, 1055: 147-166.

[12] Basagiannis S, Katsaros P, Pombortsis A. An Intruder model with Message Inspection for Model Checking Security Protocols [J]. Computers & Security. 2010, 29(1): 16-34.

[13] Donini F M, Mongiello M, Ruta M, et al. A Model Checking-based Method for Verifying Web Application Design [C]. Proceeding of the International Workshops on Web Languages and Formal Methods. 2006, 151(2): 19-32.

[14] Patel R, Borisaniya B, Patel A, et al. Comparative Analysis of Formal Model Checking Tools for Security Protocol Verification [J]. Recent Trends in Network Security and Applications. Springer Berlin Heidelberg. 2010:152-163.

[15] LIU Y C. Fairness Analysis of E-Commerce Protocols based on Strand Spaces [J]. International Journal of Grid and Utility Computing. 2013, 4(2): 128-133.

[16] Matsuo S, Miyazaki K, Otsuka A, et al. How to Evaluate the Security of Real-Life Cryptographic Protocols? [J]. Financial Cryptography and Data Security. 2010:182-194.

[17] Abadi M, Gordon A D. A Calculus for Cryptographic Protocols: The Spi Calculus [C]. Proceedings of the 4th ACM Conference on Computer and Communications Security. 1997:36-47.

[18] Fabrega F J T, Herzog J C, Guttman J D. Strand Spaces: Proving Security Protocols Correct [J]. Journal of Computer Security. 1999, 7(2): 191-230.

[19] SONG D X, Berezin S, Perrig A. Athena: A Novel Approach to Efficient Automatic Security Protocol Analysis [J]. Journal of Computer Security. 2001,9(1):47-74.

[20] Paulson L. Proving Properties of Security Protocols by Induction [C]. Proceedings of the IEEE Computer Security Foundations Workshop. 1997:70-83.

[21] Delicata R, Schneider S. A Formal Model of Diffie-Hellman Using CSP and Rank Functions[J]. 2003.

Security Protocol Analysis based on Formal Method

DENG Hui, ZHANG Bao-feng, LIU Hui, MAO Jun-jie, BI Hai-ying

(China Information Technology Security Evaluation Center, Beijing 100085, China)

Protocol security is the foundation for ensuring of network data security. Traditional methods based on manual analysis could no longer meet the requirements of data security. How to research, analyze and verify the security protocol and its security properties in the same formal framework is now a problem demanding prompt solution. Formal analysis provides an exact mathematical method and automatic tool for solving this peoblem. In this paper, the existing formal analysis methods for security protocol are reviewed and summarized. In addition, the future researches in the three fields of equivalence verification, protocol optimization, and accuracy enhancement are also suggested.

security protocol; security analysis; formal method; network security

2015-03-24；

2015-07-25 Received date:2015-03-24；Revised date：2015-07-25

國家自然科學(xué)基金(No.61472448)

Foundation Item:National Natural Science Foundation of China(No.61472448)

TP309

A

1002-0802(2015)09-1068-05

鄧 輝(1985—)，女，博士，助理研究員，主要研究方向?yàn)樾畔踩?/p>

張寶峰(1983—)，男，碩士，副研究員，主要研究方向?yàn)樾畔踩?/p>

劉 暉(1976—)，女，博士，副研究員，主要研究方向?yàn)樾畔踩?/p>

毛軍捷(1982—)，男，博士，副研究員，主要研究方向?yàn)樾畔踩?/p>

畢海英(1981—)，女，碩士，助理研究員，主要研究方向?yàn)樾畔踩?/p>

10.3969/j.issn.1002-0802.2015.09.017