調和安全協議兩種分析方法的理論研究

摘要：安全協議形式化分析方法分為兩種，即符號方法和計算方法。比較兩種方法，它們各有優缺點。目前，將兩者進行組合優化，建立統一的調和方法框架對安全協議進行分析是研究的熱點和難點。針對該問題，對目前國際上流行的相關方法進行了分類總結，并對涉及到的技術手段進行了全面分析。

關鍵詞：安全協議； 符號方法； 計算方法； 密碼學可靠性

中圖分類號：TP309文獻標志碼：A

文章編號：1001－3695(2008)03－0930－04

安全協議形式化分析研究領域存在兩種完全不同的方法：a)符號方法，大多基于DolevYao模型，采用模型檢測或定理證明來分析安全協議；b)計算方法，基于計算復雜性理論，安全證明采用歸約分析。這兩種方法各有優缺點：符號方法可有效實現自動化，但會遺漏從底層密碼算法或密碼算法與協議的交互中產生的一些安全問題，不能真正建立起密碼學的可靠性；計算方法是密碼學可靠的，但多采用手工證明，自動化程度較低。因此，結合兩種方法的優點，將兩者組合到一個框架中對安全協議進行形式化分析就成為當前備受關注的研究內容。

目前對于符號方法與計算方法的調和方法研究主要集中在兩個方面：一方面側重于符號方法的調和方法研究；另一方面側重于計算方法的調和方法研究。

1側重符號方法的調和方法研究

側重符號方法的調和方法是從符號方法的角度來減少分析安全協議時所作的基本假設（如假設密碼系統是完美的），在較低的抽象層次上對安全協議進行形式化分析，改善形式化證明與協議具體執行過程的聯系，從而建立起形式化方法的密碼學可靠性。目前，研究方法主要有邏輯、模擬、LMMS以及密碼學擴充四種方法。前三種是研究的主流方法，其主要思想是用理想功能和不可區分來描述證明協議的組合安全性質，即實際協議的安全性通過與理想協議或理想功能的對比來描述。

1．1邏輯方法

在邏輯方法框架中定義了邏輯集合和計算集合，邏輯描述可以在計算集合中表示。如果在邏輯集合中可以證明出某安全命題，則在計算集合中此安全命題的計算解釋也是有效的。邏輯方法的優點在于邏輯上的簡潔性；其缺點在于邏輯上的抽象性過高，這種抽象往往會掩蓋(或丟失)協議執行的狀態信息，難以完全反映協議運行的全貌。這方面的代表性方法是AbadiRogaway方法。

1．1．1AbadiRogaway方法

M. Abadi等人[1]于2000年首次綜合符號方法和計算方法，提出了AbadiRogaway方法。此方法證明了如果兩個表達式在邏輯公式下等價，則在計算復雜性下它們所生成的概率分布也是計算不可分的。

它首先在邏輯模型中定義一個表達式類和表達式等價關系。表達式代表數據，由原子消息和密鑰通過對偶、對稱加密構建。接著為形式化的消息定義了模式pattern（pattern由原子消息、密鑰、對偶、對稱加密以及不可解密組成。形式化消息的pattern比消息本身的結構簡單。直觀上，pattern是表達式集合的擴展，它增加了攻擊者不能解密的消息表達式類型）。表達式等價當且僅當它們能產生相同的pattern。此等價關系抓住了對攻擊者而言數據看起來一樣這一特征。邏輯模型中的這些定義十分簡單，不需要概率和計算復雜性的任何概念。

隨后用bit串、概率和復雜性描述了一個計算模型。在計算模型中定義了計算上不可區分的加密，定義與邏輯模型語義上的安全類似。表達式E的計算語義為概率分布總體{Π(η)}η。其中：Π=(K，ε，D)；K是密鑰生成算法，輸入安全參數η，輸出一個隨機密鑰k；ε是加密算法；密鑰K和明文m為輸出；D是解密算法；η∈N。

最后將等價與計算不可區分相聯系，其可靠性定理表明等價表達式蘊涵計算不可區分，即如果兩個表達式在邏輯公式下等價，則它們在計算的解釋下，根據計算不可區分的標準概念也是等價的，記為MN，則Π≈Π。

此工作增強了符號方法的密碼學基礎，但其可靠性定理僅允許對簡單協議進行建模。M. Abadi等人[2]隨后將此工作擴展到更復雜的協議中，即幾個參與方通過加/解密與發送消息相互通信。但與AbadiRogaway方法一樣，它僅考慮了被動攻擊者、對稱加密及同步調度。

1．1．2擴展工作

針對Abadi工作的不足，許多人進行了改進。

P. Laud[3]提出靜態分析技術，在主動攻擊者之下建立對稱加密原語的密碼學可靠性。此方法是關于復雜性理論下的安全性，并用于檢測協議安全。與AbadiRogaway相似，該方法也為協議定義了pattern，將協議的安全性證明轉換為pattern安全性證明，轉換的正確性以對稱加密的安全定義為基礎。這種轉換的優點在于為協議分析提供了完全自動的方式，即使在主動攻擊下分析結果也是正確的。然而該方法的缺點也不容忽視，它只能用于對稱加密，且會話次數受限。

D. Micciancio等人[4]指出AbadiRogaway邏輯的不完備性，給出了完備的條件，并證明了如果使用充分強的加密方案，任何兩個表達式計算等價當且僅當它們可以在邏輯上等價；同時，他們又進一步給出了在主動攻擊者下對安全協議的安全性進行證明的通用方法[5]。首次提出了主動攻擊條件下將簡潔的邏輯集合轉換成標準計算集合的方法，為一般的設計和評估密碼意義下的安全協議提供了理論依據。

R. Impagliazzo等人[6]則給出了用來推理關于標準密碼安全定義可靠的密碼構造兩個邏輯系統，并且通過具體的例子說明了任何利用這些系統證明基本密碼構造的行為都是正確的。他們還指出構造密碼學可靠的形式系統存在五方面困難：a)安全定義的形式描述；b)安全定義中概率的使用；c)隨機選擇和隨機分布的推理；d)量化攻擊者的計算能力；e)歸納法直觀而危險的錯誤使用。通過結果分析，表明形成一個蘊涵處理這些難點的邏輯系統是可能的。 1．2模擬方法

模擬方法的特點是首先構建一個安全的理想系統，通過比較攻擊者同實際系統交互時能夠得到的結果與攻擊者同理想系統交互時能夠得到的結果，來分析與證明實際系統相對于理想系統的安全性。這方面的代表性方法有BPW方法和Canetti方法。

1．2．1概率互模擬模型BPW方法

BPW方法[7]由M. Backes等人于2003年首次提出。該方法規范了一個抽象的密碼學可靠的密碼庫（cryptographic library）。此密碼庫由DolevYao模型的要素構成，第一次涵蓋了主動攻擊和嵌入式操作符，在任意主動攻擊者存在的情況下，任意協議環境下對于任意安全性質均能以密碼實現。其證明過程是一個新穎、概率的不完全互模擬與密碼歸約和靜態信息流分析的組合。此密碼庫包括公鑰加密、數字簽名、時鮮值、列表操作和應用數據。主體的行為環境是交互式的，建立的模型包括主體模型、交互模型以及敵手模型。安全性的刻畫利用模擬的思想和計算不可區分的機制實現，如圖1所示。

系統Sys由結構組成，而結構由機器集合M和自由端口的子集S組成，每個機器均是一個隨機I/O自動機（PIOM）。對任意結構M1，S∈Sysreal，任意多項式時間內的用戶H，任意多項式時間內的攻擊者A1，存在一多項式時間內的攻擊者A2，且M2，S∈Sysid使得Viewreal(H)和Viewideal(H)計算不可區分。

BPW方法主要包括以下三個方面的研究：

a)分析復雜協議，實現自動化驗證。目前BPW方法已成功應用于分析NS協議、OtwayRees協議、電子支付協議以及Kerbros協議。盡管BPW模型與一般的DolevYao模型相比增加了操作符和規則，但協議的自動化證明是可行的，而且密碼學基礎也更為可靠。文獻[8]主要研究了在異步網絡中如何實現對安全協議的合理密碼學抽象，并用PVS實現了對BPW模型的半自動化驗證。文獻[9]提出了用類型系統檢測基于BPW模型的協議安全，首次提出用自動化方法分析BPW密碼庫的思想，但未考慮類型推論，不能自動執行協議。文獻[10]將BPW模型嵌入到定理證明器Isabelle中，第一次實現了NS協議的自動運行。最新的研究成果是在文獻[11]中提出的通過自動化流分析驗證協議安全性的一種新方法。該方法證明了基于BPW的密碼學可靠性的信息安全，安全定義也更為細粒化，但未完全實現全自動方式證明。

b)將更多密碼原語并入密碼庫。在原有基礎上，BPW密碼庫中加入了對稱加密、認證、hash、XOR等新的原語。因為在原來的BPW模型中這些原語不能被模擬，通過限制環境條件來放寬模擬，即條件反應性模擬（conditional reactive simulata￣bility），并證明了在條件模擬下，組合定理也是成立的。以對稱加密原語為例[12]，對稱原語在BPW通用密碼庫中很難理想化，這可通過模擬器(simulator)進行證明，模擬器與理想系統和實際系統進行交互，將實際系統的攻擊者看做黑箱子系統，模擬實際系統中所有可見行為。對對稱加密而言，如采用模擬，當理想系統允許在任意時間傳遞密鑰（典型DolevYao系統允許在任意時間傳遞有效項）時，則會發生承諾問題。誠實主體首先發送一份攻擊者可以看到的密文；然后發送其包含的明文和密鑰，攻擊者就可解密出明文。這在實際協議中是會發生的。模擬器對此過程進行模擬的具體步驟如下：在知道密文發送后用一些隨機的比特串進行模擬；然后模擬器發現密鑰已被知道，在此情況下它必須隨機選取1 bit串來模擬與此密文相對應的確定密鑰。這基本是不可能的。在此情況下，BPW為了模擬對稱加密，通過加強假設來排除承諾問題的發生，這在另一方面說明了BPW的局限性。

c)對協議的其他性質進行驗證（概率信息流[13]和無干擾[14]）。信息流與無干擾是描述完整性和保密性的重要技術。信息流闡述了秘密性，即如果沒有信息流從秘密系統流向安全性更弱的系統，或從高級別用戶流向安全性更弱的用戶，則稱協議滿足秘密性。無干擾闡明了完整性，即如果沒有不可信的信息干擾可信度更高的用戶，則稱協議滿足完整性。

1．2．2Canetti方法

R.Canetti[15]提出了分析密碼協議的新模型——universally composable security（UC）。UC的顯著特征是當安全協議與協議的任何集合組合時，或當安全協議作為任意系統的組成部分時，可確保協議的復合安全。這對保持在如網絡這種復雜不可預測的系統中密碼協議的安全性是十分重要的。UC可以有效地描述現實中的很多協議，包括認證通信（authenticated communication）、密鑰交換(key exchange)、保密通信（secret communication）、數字簽名（digital signatures）、承諾（commitment）、健忘傳輸（oblivious transfer）、零知識（zero knowledge）、可驗證的秘密共享（verifiable secret sharing）及安全功能評估（secure function evaluation）等。

UC基于概率多項式時間下交互圖靈機（PITMS）。它包括一個實際協議和一個理想功能、一個實際攻擊者和一個理想攻擊者、一個環境。從以下幾個方面對協議進行描述：

a)計算復雜性理論下的協議規范。協議就是一個交互式圖靈機（interactive Turin machines）的集合。

b)攻擊模型（adversarial model）。它是按計算復雜性理論方式進行描述的，與具體協議無關。它要求：網絡是異步的；通信是公開的，但未經認證的；攻擊者是主動的；攻擊者和環境作為交互式圖靈機，它們的輸出計算是按概率多項式時間算法進行的。

c)安全的定義。在協議實際運行的模型中，如果π為n方協議，記REALπ，A，Z(k，z，r)為在安全參數K、輸入Z及隨機輸入r=rz，rA，r1，…，rn的前提下，環境與攻擊者A和協議的n個交互式圖靈機交互時環境z的輸出。在協議的理想運行模型中，IDEALF，S，Z(k，z，r)為在安全參數K、輸入Z及隨機輸入r=rz，rs，rF的前提下，環境與攻擊者S和理想化功能F交互時環境z的輸出。協議運行環境利用一個環境機器z模擬。這個環境機器同時還擔任區分器的作用。如果沒有哪個環境機器能夠區分開IDEALF，S，Z(k，z，r)和REALπ，A，Z(k，z，r)，那么，這個協議就安全地實現了一個理想的功能（屬性）。

1．2．3BPW方法與Canetti方法的關系

BPW方法的實質是基于概率多項式時間I/O自動機（PIOA） 的黑箱能動模擬（BRSIM）；而Canetti方法的實質是基于概率多項式時間交互圖靈機（PITM）的通用組合（UC）。兩者均采用模擬思想和組合定理，都是在計算意義下證明協議的安全性；其主要區別在于BPW方法中理想攻擊者可依賴于環境，而Canetti方法中理想攻擊者不依賴于環境。當環境運行時間依賴于輸入消息的長度時，UC和BRSIM等價。

這兩種方法的優點在于它們所提供的通用性和強組合性，缺點在于：兩者定義均不夠清晰簡潔；定義推導均包括一個模擬器，而模擬不是在任何時候都直觀的，如對零知識而言，模擬是直觀的，但當定義承諾問題時，就需要更多的技術來實現。

1．3LMMS：概率多項式時間下進程演算方法

LMMS方法的原理是將概率函數直接引入系統中，用概率多項式時間的進程運算對安全協議進行分析。該方法沿用了計算密碼學的思想，其目標是提供一種與標準密碼學假設相吻合的安全協議分析的形式，開發一種表達概率多項式時間協議步驟的語言，發展一種關于等價的可復合的描述手段，并建立關于等價的推理方面的邏輯基礎。該方法的優點在于描述協議十分精確；缺點在于其抽象規范包含密碼細節，正確性相對較難驗證。

P.Lincoln等人[16]于1998年建立了可用于研究協議與密碼原語交互的分析框架，并提出了一個基于密碼學的形式模型。在這個模型中，攻擊者是任意概率多項式時間的進程，協議以進程演算的形式表達，協議安全以觀察等價（observational equivalence）的方式描述，通過概率等價的漸近性，將觀察等價與多項式時間的統計測試相聯系。該方法類似于SPI演算，也是用進程演算和觀察等價來描述安全性質。主要區別在于前者是基于復雜性理論，增強了攻擊者能力，允許攻擊者通過靜態分析網絡流量來收集信息，且根據攻擊成功概率來定義協議安全；而后者則是以完美假設為前提。J. Mitchell等人[17]基于通信系統演算（CCS）語言，將進程中不確定性替換為隨機性并提出了推理觀察等價的機制。

1．4形式化方法的密碼學擴充

密碼學擴充包括DolevYao模型擴充和形式化方法擴充，它可充分利用現有技術，但也同時導致復雜性的急劇膨脹。

DolevYao模型擴充是在原有系統中增加密碼學要素，以增加系統的表達能力。例如，在串空間模型的研究中[18]，直觀定義honest函數，使其擴充的串空間模型能分析使用異或和指數函數的協議；文獻[19]將密碼協議與協議中用到的密碼算法視為一個系統，基于組合推理技術建立了密碼協議系統的形式化模型。形式化方法擴充的目的在于囊括更為廣泛的密碼算法。文獻[20，21]對邏輯方法進行了擴充；文獻[22]對模型檢測進行了擴充。

2側重計算方法的調和方法研究

側重計算方法的調和方法研究主要是從計算方法的角度發展處理復雜問題的高層推理技術，其代表性方法是RO（隨機問答器）方法和Bruno方法。

2．1RO方法

RO方法[23]的原理是假定各方共同擁有一個公開的RO，就可以在密碼理論與應用之間架起一座橋梁。在RO模型中的歸約論斷一般表現為：首先形式化定義方案的安全性，假設概率多項式時間（PPT）下攻擊者能夠以不可忽略的概率破壞協議的安全性；然后模仿者（就是設計者或分析者）為攻擊者提供一個與實際環境不可區分的模擬環境，回答攻擊者的所有oracle詢問；最后利用攻擊者的攻擊結果（即適當選擇的函數h）設法解決諸如大數分解之類的基礎難題。如果將RO模型換成現實模型就得到標準安全性證明。此方法提出了具體安全性這個重要概念，可以得到較準確的安全度量，但并不能保證完備性，RO模型中的安全性與通過具體實現的安全性之間無必然的因果關系。

2．2Bruno方法

B.Bruno[24]于2005年提出了一種新的密碼協議安全性自動化驗證工具。該驗證器基于密碼協議的計算模型，在主動攻擊下分析協議安全，并可以給出博弈序列形式的證明過程，這些博弈序列采用概率多項式時間演算進行形式化。攻擊者被看做一個在概率多項式時間（PPT）內運行完成的有效算法；安全性條件則被描述為攻擊者可以執行給定計算的可能性。安全性的定義表明即使攻擊者可以選擇m0和m1，他也應當無法區分對消息m0的加密與對消息m1的加密。此驗證器無須進行額外的前提假設，但缺點是當協議不滿足安全特性時不能給出相應的攻擊路徑。

3結束語

在安全協議形式化分析時，符號方法和計算方法各有優缺點，單獨運用符號方法或計算方法不能完全保證分析結果的正確性和完備性。針對該問題，圍繞符號方法和計算方法的調和方法研究，本文詳細介紹了六種代表性方法，全面分析了方法的原理和技術特點。各種方法的比較結果如表1所示。

參考文獻：

[1]ABADI M， ROGAWAY P. Reconciling two views of cryptography

(The computational soundness of formal encryption)[C]//Proc of the 1st IFIP International Conference on Theoretical Computer Scie￣nce.[S.l.]: Springer， 2000: 3－22.

[2]ABADI M， JURJENS J. Formal eavesdropping and its computational interpretation[C]//Proc of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS). 2001: 82－94 .

[3]LAUD P. Symmetric encryption in automatic analyses for confidentia￣lity against active adversaries[C]//Proc of 2004 IEEE Symposium on Security and Privacy. 2004: 71－85.

[4]MICCIANCIO D， WARINSCHI B. Completeness theorems for the AbadiRogaway logic of encrypted expressions[J]. Journal of Computer Security， 2004，12(1):99129.

[5]MICCIANCIO D， WARINSCHI B. Soundness of formal encryption in the presence of active adversaries[C]//Proc of Theory of Cryptography Conference(TCC). Cambridge，Massachusetts:[s.n.]， 2004:133151.

[6]IMPAGLIAZZO R， KARPON R. Logics for reasoning about cryptographic constructions[C]//Proc of STOC’03. San Diego， California:[s.n.]， 2003: 372－383.

[7]BACKES M， PFITZMAN B， WAIDNER M. A composable cryptographic library with nested operations (extended abstract)[C]//Proc of the 10th ACM Conference on Computer and Communications Secu￣rity. 2003: 220－230.

[8]BACKES M， JACOBI C. Cryptographically sound and machineassisted verification of security protocols[C]//Proc of the 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS). 2003:675－686.

[9]LAUD P. Secrecy types for a simulatable cryptographic library[C]//Proc of the 12th ACM Conference on Computer and Communications Security. 2005: 26－35.

[10] SPRENGER C， BACKES M， BASIN D， et al. Cryptographically sound theorem proving[C]//Proc of the 19th IEEE Computer Security Foundations Workshop (CSFW). 2006.

[11] BACKES M， LAUD P. Computationally sound secrecy proofs by mechanized flow analysis[C]//Workshop on Formal and Computational Cryptography (FCC’06). Venice:[s.n.]， 2006.

[12] BACKES M， PFITZMAN B. Symmetric encryption in a simulatable DolevYao style cryptographic library[C]//Proc of the 17th IEEE Computer Security Foundations Workshop (CSFW). 2004: 204－218.

[13] BACKES M. Quantifying probabilistic information flow in computational reactive systems[C]//Proc of the 10th European Symposium on Research in Computer Security(ESORICS 2005).2005: 336－354.

[14] BACKES M， PFITZMAN B. Computational probabilistic noninterfe￣rence[C]//Proc of the 7th European Symp Research in Computer Security (ESORICS). 2002: 1－23.

[15] CANETTI R. Universally composable security: a new paradigm for cryptographic protocols[C]//Proc of the 42nd IEEE Symposium on Foundations of Computer Science (FOCS). 2001: 136145.

[16] LINCOLN P， MITCHELL J， MITCHELL M， et al. A probabilistic polytime framework for protocol analysis[C]//Proc of the 5th ACM Conference on Computer and Communications Security. 1998: 112121.

[17] MITCHELL J， RAMANNATHAN A， SCEDROV A， et al. A probabilistic polynomial time calculus for analysis of cryptographic protocols(preliminary report)[C]//Proc of the 17th Annual Conference on the Mathematical Foundations of Programming Semantics. Arhus， Denmark:[s.n.]， 2001.

[18] MANEKI A P. Honest functions and their application to the analysis of cryptographic protocols[C]//Proc of the 12th IEEE Computer Security Foundations Workshop(CSFW 1999). Mordano:[s.n.]， 1999: 83－89.

[19] 劉怡文， 李偉琴. 密碼協議的一種基于組合推理的模型驗證[J]. 通信學報，2003，24(9):122127.

[20] OORSCHOT P V. Extending cryptographic logics of belief to key agreement protocols(extended abstract)[C]//Proc of the 1st ACM Conference on Computer Communications Security.Fairfax， Virginia: ACM， 1993:232－243.

[21] SYVERSON P， OORSCHOT P V. On unifying some cryptographic protocol logics[C]//Proc of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Washington D C:[s.n.]，1994: 14－28.

[22] MEADOWS C. Analysis of the Internet key exchange protocol using the NRL protocol analyzer[C]//Proc of Symp on Security and Privacy. 1999: 216－213.

[23] BELLARE M， ROGAWAY P. Random oracles are practical：a paradigm for designing efficient protocols[C]//Proc of the 1st ACM Conf on Computer and Communications Security. New York: ACM Press， 1993: 62－67.

[24] BRUNO B. A computationally sound mechanized prover for security protocols[C]//Proc of IEEE Symposium on Security and Privacy (SP). [S.l.]:IEEE Computer Society Press， 2006.

“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”