夏 銳，錢振江，2，劉 葦

（1.蘇州大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 蘇州 215000；2.常熟理工學(xué)院 計算機(jī)科學(xué)與工程學(xué)院，江蘇 常熟 215500；3.國網(wǎng)電力科學(xué)研究院，南京 211000）

0 概述

隨著信息技術(shù)的不斷發(fā)展，數(shù)字化信息借助互聯(lián)網(wǎng)絡(luò)進(jìn)行廣泛傳播，信息安全逐步成為公眾關(guān)注的焦點，而通信協(xié)議對于確保信息安全起著至關(guān)重要的作用。通信雙方在進(jìn)行信息交互時會遵守事先約定的通信協(xié)議，但這并不能保證信息交互過程的絕對安全，很多重要信息仍會面臨被盜取的風(fēng)險，并且通信協(xié)議本身可能就存在某些安全漏洞，因此通信協(xié)議的安全性分析技術(shù)應(yīng)運(yùn)而生。

安全通信協(xié)議的形式化分析是信息安全領(lǐng)域的重要研究方向，根據(jù)技術(shù)特點可分為定理證明和模型檢測兩類。定理證明是一項以數(shù)學(xué)為基礎(chǔ)的技術(shù)，主要是在邏輯層面驗證程序是否正確［1］。在形式化驗證研究領(lǐng)域，定理的機(jī)械證明作為形式化驗證方式，主要通過人工方式和驗證工具進(jìn)行交互對數(shù)學(xué)定理進(jìn)行半自動的推理和證明，進(jìn)而在邏輯關(guān)系上對定理的正確性做出判斷［2］。定理證明方法的工作重點在于對安全通信協(xié)議中出現(xiàn)的實體對象進(jìn)行形式化表示，將實體抽象成數(shù)據(jù)對象并使用形式化操作語義描述實體行為［3］。對象建模和行為抽象是驗證工作的核心步驟，根據(jù)期望性質(zhì)建立定理并采用形式化策略證明其正確性是驗證工作的關(guān)鍵。模型檢測方法的優(yōu)點是檢測過程完全自動化，但只能處理有限狀態(tài)的系統(tǒng)，在應(yīng)用過程中需要對檢測范圍加以限制［4］，并且模型檢測方法可直觀地發(fā)現(xiàn)通信協(xié)議的安全漏洞，然而其最大的弊端在于即使沒有發(fā)現(xiàn)通信協(xié)議漏洞，也不能確保通信協(xié)議絕對安全。為更全面地對通信協(xié)議進(jìn)行邏輯上的安全性分析，本文使用Isabelle/HOL 定理證明輔助工具［5］對D_protocol 混合密鑰加密協(xié)議建立通信代理和消息序列的形式化模型，并采用規(guī)則歸納方式驗證該通信協(xié)議的安全性。

1 相關(guān)工作

形式化驗證通信協(xié)議的主要任務(wù)是對通信協(xié)議中涉及的實體對象、消息、動作、知識狀態(tài)和信任關(guān)系等進(jìn)行邏輯抽象［6］。近年來，已有很多專家和學(xué)者對通信協(xié)議安全性進(jìn)行驗證研究并取得了重要成果。文獻(xiàn)［7］采用以RDP 協(xié)議為基礎(chǔ)的仿真技術(shù)還原了RDP 協(xié)議的數(shù)據(jù)信息，研究結(jié)果表明RDP 協(xié)議存在中間人攻擊的漏洞，因此作者在此基礎(chǔ)上利用綁定IP 地址和修改端口號的方式對其進(jìn)行改進(jìn)。文獻(xiàn)［8］基于二重特征值的思想，提出一種三方密鑰交換協(xié)議，其既可抵御中間人攻擊，又可進(jìn)行用戶合法性認(rèn)證。該協(xié)議通過生成新的會話密鑰以避免舊密鑰多次使用的安全隱患，并通過對比分析的方式證明該協(xié)議具有良好的安全性和高效性。

傳統(tǒng)匿名認(rèn)證協(xié)議存在匿名不可控和通信時延大等問題。文獻(xiàn)［9］提出的基于異構(gòu)無線網(wǎng)絡(luò)的可控漫游認(rèn)證協(xié)議解決了以上問題，該協(xié)議僅需一輪消息交互即可完成對移動終端的身份合法性認(rèn)證，并借助CK 安全模型驗證了該協(xié)議的可靠性。文獻(xiàn)［10］在分析Li 匿名協(xié)議的安全缺陷基礎(chǔ)上，提出一種基于共享密鑰的輕量級匿名認(rèn)證方案，并通過安全分析和仿真測試對方案可靠性進(jìn)行驗證，結(jié)果表明其可抵御時間關(guān)聯(lián)等攻擊，且具有較小的計算量和存儲開銷。文獻(xiàn)［11］從理論分析角度研究TCP/NC 協(xié)議的吞吐量模型，模型仿真和理論分析結(jié)果均表明網(wǎng)絡(luò)編碼可有效提升傳統(tǒng)TCP 協(xié)議的安全性能。文獻(xiàn)［12］提出一種抵御中間人攻擊的可信網(wǎng)絡(luò)連接協(xié)議S-TNC，在生成協(xié)商密鑰的基礎(chǔ)上導(dǎo)出會話密鑰實現(xiàn)認(rèn)證端和通信端的綁定。分析結(jié)果表明，S-TNC 協(xié)議相比現(xiàn)有協(xié)議未增加新的實體和證書，并且具有較高的安全性。

傳統(tǒng)對稱密鑰管理方案存在存儲空間占用大、安全性低等問題。文獻(xiàn)［13］提出基于對稱和非對稱密碼體制的密鑰管理方案，當(dāng)該方案應(yīng)用于無線傳感器網(wǎng)絡(luò)時，使用公開的臨時主密鑰對節(jié)點公鑰進(jìn)行身份認(rèn)證，而節(jié)點間信息交互使用的成對密鑰是基于非對稱密碼技術(shù)建立。實驗結(jié)果表明，該方案較好地解決了傳感器節(jié)點的計算限制問題，但作者未對其可靠性證明展開進(jìn)一步研究。文獻(xiàn)［14］提出的密鑰生成（SKG）協(xié)議利用對稱的臨時密鑰認(rèn)證網(wǎng)絡(luò)中的節(jié)點，而實際的會話密鑰使用非對稱密碼技術(shù)建立。仿真結(jié)果表明，SKG 協(xié)議雖然提高了網(wǎng)絡(luò)吞吐量并且降低了密鑰分配功耗，但該協(xié)議缺少安全性證明。文獻(xiàn)［15］提出一種新的可驗證多秘密共享（Verifiable Multi-Secret Sharing，VMSS）方案，該方案以橢圓曲線加密系統(tǒng)為基礎(chǔ)，在縮短密鑰長度的情況下保證了協(xié)議具有良好的抗攻擊性，最終通過建立數(shù)學(xué)定理驗證了該方案的正確性。文獻(xiàn)［16］證明了雙因素身份認(rèn)證方案存在去同步攻擊問題，并且其容易受到特權(quán)內(nèi)幕攻擊和已知的密鑰攻擊。為解決以上問題，WANG 等人提出一個具有可證安全性的增強(qiáng)方案，該方案在沒有增加額外計算成本的情況下具有較高的安全性和隱私性。文獻(xiàn)［17］提出一種雙因素認(rèn)證方案的評估框架，該框架由12 條標(biāo)準(zhǔn)集和1 個對手模型組成，可及時發(fā)現(xiàn)服務(wù)器信息泄露并阻止離線猜測問題的發(fā)生。

現(xiàn)有研究表明：由于靜態(tài)共享密鑰和短暫臨時密鑰的存在，因此導(dǎo)致YAK 公鑰身份認(rèn)證協(xié)議存在一定的安全隱患，且不能抵御所有已知攻擊。文獻(xiàn)［18］通過加強(qiáng)驗證機(jī)制和實體身份認(rèn)證等對YAK 協(xié)議進(jìn)行改進(jìn)，并且在Diffie-Hellman 隨機(jī)預(yù)言假設(shè)下驗證了YAK 協(xié)議的安全性。文獻(xiàn)［19］以現(xiàn)有EuroRadio 安全通信協(xié)議為基礎(chǔ)，設(shè)計并實現(xiàn)了一套適用于無線調(diào)車機(jī)車信號和監(jiān)控系統(tǒng)（STP）的安全通信協(xié)議，采用ASK-CTL 時序邏輯對協(xié)議進(jìn)行形式化驗證，結(jié)果表明該協(xié)議在一定的信道干擾條件下仍可實現(xiàn)功能安全。為更好地研究第二代內(nèi)殼協(xié)議（SSHV2）的安全性，文獻(xiàn)［20］采用Blanchet 演算方式對協(xié)議流程進(jìn)行分析，并借助CryptoVerif 建模工具模擬協(xié)議執(zhí)行過程，驗證結(jié)果表明該協(xié)議可實現(xiàn)服務(wù)端對客戶端的認(rèn)證，并且具有較高的安全性。

2 通信協(xié)議

2.1 協(xié)議簡介

密鑰加密算法包括對稱加密算法和非對稱加密算法［21］兩類。對稱加密算法是一種傳統(tǒng)的密碼加密算法，主要分為加密和解密密鑰相同及通過算法從解密密鑰中計算得到加密密鑰兩種類型。在通常情況下，對稱算法中加密和解密過程使用相同的密鑰，因此該算法也被稱為單密鑰算法。對稱密鑰算法要求通信雙方在進(jìn)行安全通信前商定一個密鑰，該密鑰的保密性直接決定通信過程是否安全。如果泄露密鑰，則惡意攻擊者就能對消息進(jìn)行加密或解密，甚至可以對原始消息進(jìn)行篡改以欺騙其他用戶。因此，在對稱密鑰體制下，為保證通信過程安全可靠，密鑰必須嚴(yán)格保密。相對非對稱加密過程而言，對稱加密算法的密鑰長度較短，數(shù)據(jù)計算量較小，加密速度較快。然而，不同用戶之間需要使用特定的密鑰進(jìn)行消息處理，由此導(dǎo)致密鑰數(shù)量大、不易管理的問題。非對稱加密算法采用公鑰加密和私鑰解密的技術(shù)，其中，公鑰對協(xié)議網(wǎng)絡(luò)中其他用戶公開，私鑰僅由用戶保管，在非對稱加密過程中由于公鑰通常復(fù)雜度較高，因此在消息加密和解密時計算量較大。非對稱加密算法基于公鑰加密和私鑰解密的特點，適用于用戶間身份認(rèn)證及無事先約定的秘密通信等場景。本文基于混合密鑰思想構(gòu)造D_protocol 協(xié)議，通信雙方各有公開密鑰（Pubkey）和私有密鑰（Prikey）兩個密鑰。除此之外，D_protocol 協(xié)議還包括一條雙方代理共享的臨時密鑰Temkey。

1）公開密鑰：所有人可知，用于對明文消息的加密操作。

2）私有密鑰：密鑰持有者可知，用于對收到的加密消息進(jìn)行解密操作。

3）臨時私有密鑰：通信代理的一方產(chǎn)生該密鑰并發(fā)送給另一方，僅由雙方代理共享，用于消息加密和解密操作。

為確保消息的實時性，避免出現(xiàn)由多條舊消息組成的虛假消息的現(xiàn)象，D_protocol協(xié)議中將引入一次性隨機(jī)數(shù)的概念，在隨機(jī)數(shù)的字節(jié)長度足夠長的情況下，特定的隨機(jī)值在一次通信過程中連續(xù)出現(xiàn)的概率可近似為0。消息包含一組新生成的隨機(jī)數(shù)來說明其不是重復(fù)發(fā)送的過時消息，隨機(jī)數(shù)作為確保消息實時性的重要信息，需要被加密存放在消息體中。

2.2 協(xié)議內(nèi)容

D_protocol 協(xié)議使用公鑰加密和私鑰解密技術(shù)，執(zhí)行過程具體為：在建立通信前，需要使用非對稱密鑰加密手段確定通信雙方代理的身份，而在消息交互過程中采用臨時密鑰加密方式，其運(yùn)行流程相對簡單且不涉及可信第三方。以具體的通信過程為例，如D_protocol 協(xié)議用戶Tom 希望與用戶Dick 建立通信，則消息交互過程如圖1 所示，采用如下半形式化方式進(jìn)行描述：

Message 1：Tom→Dick：Pubkey_D｛random_T，Tom｝

Message 2：Dick→Tom：Pubkey_T｛random_T，Temkey，Dick｝

Message 3：Tom→Dick：Temkey｛random，Tom｝

Message 4：Dick→Tom：Temkey｛random｝

圖1 用戶消息交互過程Fig.1 Process of user message interaction

以上通信過程是結(jié)合對稱密鑰算法和非對稱密鑰算法的具體應(yīng)用實例。消息中多次加入了發(fā)送方簽名，目的在于防止用戶將消息發(fā)送給不可信任的用戶，這些不可信任的用戶代理可能會將消息進(jìn)行存儲轉(zhuǎn)發(fā)給其他協(xié)議用戶，從而引起消息內(nèi)容泄露，即中間人攻擊。以具體的通信過程為例，如D_protocol 協(xié)議用戶Tom 希望與用戶Dick 建立通信，間諜Harry 竊聽消息并對其進(jìn)行轉(zhuǎn)發(fā)，則消息交互過程如圖2 所示。

圖2 中間人攻擊過程Fig.2 Process of man in the middle attack

在消息中加入用戶簽名后，如果接收方解密消息，發(fā)現(xiàn)消息發(fā)送者不是約定好的用戶代理時便終止通信過程，該方式可以有效避免內(nèi)部攻擊的發(fā)生。在傳統(tǒng)公鑰加密過程中，由于公鑰長度過長，因此導(dǎo)致加密數(shù)據(jù)量較大的信息時加密速度慢，嚴(yán)重影響通信效率。D_protocol 協(xié)議克服了公鑰加密過程復(fù)雜的問題，在確認(rèn)通信方身份后，利用對稱密鑰加密算法對消息進(jìn)行加密，由于對稱密鑰可在很短時間內(nèi)完成加密和解密操作，因此當(dāng)傳輸信息量較大時能明顯提高通信效率。本文使用Isabelle/HOL 定理證明輔助工具對D_protocol 協(xié)議進(jìn)行形式化建模，采用規(guī)則歸納方式驗證其安全性。

2.3 協(xié)議安全性分析

從算法角度而言，D_protocol 協(xié)議屬于以密碼學(xué)相關(guān)知識為基礎(chǔ)的密鑰加密算法，在不發(fā)生密鑰泄露的情況下通信過程不可攻擊。D_protocol 協(xié)議將對稱密鑰加密技術(shù)和非對稱密鑰加密技術(shù)進(jìn)行結(jié)合，使用非對稱加密技術(shù)確定用戶身份并傳輸隨機(jī)生成的共享單密鑰，以臨時單密鑰的方式對通信主體過程進(jìn)行消息加密操作。首先考慮非對稱加密過程的安全性，用戶的公開密鑰對其他用戶而言是透明的，而私有密鑰不對外界公開，僅由持有者可知。公開密鑰復(fù)雜度較高，導(dǎo)致加密算法的運(yùn)行速度緩慢。密鑰的高復(fù)雜度也使得協(xié)議攻擊者無法在合理的時間范圍內(nèi)由公開密鑰推導(dǎo)出私有密鑰，即使協(xié)議攻擊者捕獲了密文消息也無法對其進(jìn)行解密操作。而對稱加密算法的加密過程和解密過程使用相同密鑰，該密鑰僅由通信雙方掌握，一旦泄露則消息內(nèi)容就會被輕易竊取。由于對稱加密的密鑰復(fù)雜度相對較低，因此在很短時間內(nèi)即可完成加密操作，并且能大幅提升通信效率。

3 通信協(xié)議的形式化建模

在D_protocol 協(xié)議的形式化證明部分，本文首先對Isabelle/HOL 定理證明輔助工具進(jìn)行簡單介紹，然后建立用戶代理和通信消息的抽象模型，并在此基礎(chǔ)上對攻擊協(xié)議的不誠信用戶進(jìn)行形式化建模，使用集合的閉包性質(zhì)描述攻擊行為，最后對D_protocol 協(xié)議建立消息流程模型。

3.1 Isabelle/HOL 定理證明輔助工具

Isabelle/HOL 是基于高階邏輯的形式化證明系統(tǒng)，被廣泛應(yīng)用于計算機(jī)軟硬件模塊的可靠性證明及數(shù)學(xué)定理的安全性驗證等任務(wù)中［5，22］。Isabelle/HOL 具有強(qiáng)大的對象描述能力和程序規(guī)約表達(dá)能力，可以借助類型系統(tǒng)與邏輯之間的同構(gòu)關(guān)系，將定理證明的過程轉(zhuǎn)變?yōu)槌绦蚓帉懙倪^程。由于證明過程的正確性可以通過機(jī)器進(jìn)行自動檢查，因此無須依靠自動定理證明算法的正確性，驗證結(jié)果更具說服力［23］。本文證明過程主要涉及Isabelle/HOL 的歸納集合論，通過定義不同的數(shù)據(jù)類型及成員函數(shù)對D_protocol 協(xié)議內(nèi)容進(jìn)行表達(dá)。

3.2 代理和消息的形式化表示

由于所有安全通信協(xié)議規(guī)范都涉及通信消息的理論，因此本文首先定義通信協(xié)議的參與者類型ptl_agent，具體包括誠實通信代理（User）和通信協(xié)議的攻擊者（Attacker）兩個數(shù)據(jù)類型，形式化表示如下：

datatype ptl_agent=User|Attacker

D_protocol 協(xié)議使用自然數(shù)類型作為通信密鑰的數(shù)據(jù)類型，浮點數(shù)類型密鑰的安全性很強(qiáng)，但其較高的計算復(fù)雜度將會嚴(yán)重影響通信效率。由于每個用戶都有一個對外公開的公鑰和一個秘密存放的私鑰，因此定義mapK 函數(shù)將用戶公鑰映射到與之相匹配的私鑰，形式化表示如下：

type_synonym key=nat

consts mapK：："key?key"

通過定義ptl_msg 數(shù)據(jù)類型引入通信中消息的標(biāo)準(zhǔn)形式，標(biāo)準(zhǔn)消息包括由代理、密鑰、用戶生成的隨機(jī)值、復(fù)合消息及加密后的消息等信息，形式化表示如下：

datatype

ptl_msg=Define ptl_agent

Form key

Random nat

Couple ptl_msg ptl_msg

Encrypt key ptl_msg

以上消息類型中出現(xiàn)了Encrypt 加密函數(shù)，Encrypt 加密函數(shù)是單射函數(shù)。在指定加密函數(shù)的情況下，如果兩條密文消息相同，根據(jù)單射函數(shù)的性質(zhì)，則可以確定這兩條密文消息對應(yīng)的明文消息，并且其加密密鑰也相同。

理論上而言，一段加密消息只可以用一個密鑰解密，且只產(chǎn)生一段明文消息。雖然一段密文也可以用其他密鑰解密，但產(chǎn)生的通常是垃圾消息。通過在明文消息尾部添加一些冗余信息，當(dāng)使用正確密鑰對相應(yīng)的密文消息進(jìn)行解密后，則可以查出這些附加內(nèi)容。通過定義mapPu_Key 函數(shù)將用戶代理映射到與之匹配的公鑰，形式化表示如下：

consts mapPu_Key：："ptl_agent ?key"

定義NonceK 函數(shù)可將用戶代理映射到其隨機(jī)生成的臨時單密鑰，形式化表示如下：

consts NonceK：："ptl_agent ?key"

與以上函數(shù)定義類似，通過定義mapPr_Key 函數(shù)可將用戶代理映射到與之匹配的私鑰。mapPr_Key 函數(shù)是mapK 和mapPu_Key 函數(shù)的結(jié)合，形式化表示如下：

abbreviation mapPr_Key：："ptl_agent ?key"

where "mapPr_Key A ≡mapK（mapPu_Key A）"

在該通信體制下，分配用戶的密鑰必須彼此不同，這是保證通信過程安全的必要條件。任何兩個用戶代理不會有相同的公鑰，也不會出現(xiàn)不同用戶的公鑰和私鑰相同的情況。本文驗證過程使用事件軌跡的方式記錄用戶之間傳輸消息的行為過程，形式化表示如下：

datatype trace=Send ptl_agent ptl_agent ptl_message

3.3 攻擊者行為建模

在該協(xié)議證明過程中，協(xié)議攻擊者具有重要作用。攻擊者通常是了解協(xié)議內(nèi)容但不遵守協(xié)議規(guī)則的惡意用戶，通過利用協(xié)議漏洞對通信過程進(jìn)行入侵，竊取消息內(nèi)容，甚至捕獲其他代理的密鑰。除此之外，攻擊者還會使用已獲得的用戶密鑰，構(gòu)造虛假消息欺騙其他用戶，嚴(yán)重危害協(xié)議內(nèi)部的通信安全。

基于Isabelle/HOL 集合理論，構(gòu)造ptl_analyse 和ptl_create 形式化函數(shù)表示通信協(xié)議中攻擊者的入侵和欺騙行為。ptl_analyse 函數(shù)通過對消息集合進(jìn)行分析得到知識集合，而ptl_create 函數(shù)通過對消息集合中的信息進(jìn)行重組得到虛假消息集合。集合ptl_analyseM表示以消息集合M為參數(shù)，函數(shù)ptl_analyse 從集合中挖掘有用知識的過程。其閉包性質(zhì)的遞歸定義以如下形式化方式表示：

inductive_set

ptl_analyse：："ptl_msg set ?ptl_msg set"

for M：："ptl_msg set"

where

Decrypt［intro］："［|Encrypt C A∈ptl_analyse M；

Form（mapPr_Key C）∈ptl_analyse M|］?A∈ptl_analyse M"

|mp［simp］："A∈M?A∈ptl_analyse M"

|cptl："｛［A，B］｝∈ptl_analyse M?A∈ptl_analyse M"

|cptr："｛［A，B］｝∈ptl_analyse M?B∈ptl_analyse M"

在以上建模過程中，"｛［］｝"中包含內(nèi)容為傳輸消息體，消息體中可能包括一次性隨機(jī)數(shù)、用戶簽名或者隨機(jī)單密鑰等重要信息。Couple 函數(shù)為消息體，（CoupleM1，CoupleM2，…，CoupleMn）即為｛［M1，M2，…，Mn］｝，表示消息體中包含n條消息分量。

對于解密規(guī)則，攻擊者只要在捕獲用戶發(fā)送消息的前提下進(jìn)一步取得加密公鑰對應(yīng)的私鑰，就可以破解該條消息。通過規(guī)則歸納分析可以得知，ptl_analyse 函數(shù)具備單射蘊(yùn)含性質(zhì)，即如果消息集合A包含消息集合B，那么攻擊者通過分別對其進(jìn)行分析，可以獲知知識信息集合A'也必然包含知識信息集合B'。此外，ptl_analyse 函數(shù)還具有冪等性質(zhì)，即攻擊者對一個消息集合M進(jìn)行分析可得到另一個信息集合M'，但即使對M'再次進(jìn)行分析，也不會產(chǎn)生新的有用信息，形式化表示如下：

Analyse_ide：ptl_analyse(ptl_analyse M)=ptl_analyse M

與ptl_analyse 函數(shù)類似，ptl_create 函數(shù)的映射關(guān)系也是由一個消息集合指向另一個消息集合，攻擊者從消息集合中可獲知所有遵守該協(xié)議的通信代理。對Encrypt 加密函數(shù)進(jìn)行分析，假設(shè)X是攻擊者從消息集合M中生成的信息，公鑰K也屬于集合M，因此使用K加密X后的消息仍屬于虛假消息集合。由于警惕性較高的用戶不可能將私鑰作為任何消息的組成部分，也不會將沒有經(jīng)過處理的隨機(jī)值放在消息中，因此消息集合M中不包含隨機(jī)值和用戶私鑰。由上述分析可知，ptl_create 函數(shù)可以將消息集合中的信息重新組合，加密生成虛假消息，在入侵過程中用于欺騙其他用戶，并不斷擴(kuò)充知識信息集合的容量?；谝陨辖；A(chǔ)，繼續(xù)構(gòu)造ptl_piece 函數(shù)，借助該函數(shù)可以較好地分析用戶行為的正確性。集合ptl_pieceM由消息集合M的元素分量組成，除了對應(yīng)的Encrypt 構(gòu)造函數(shù)不同，該歸納函數(shù)的定義與ptl_analyse 類似，由于本文篇幅原因，具體定義過程不予給出。

3.4 事件跟隨建模

本文將D_protocol 協(xié)議的通信過程形式化為一個各項事件跟隨的集合，以時間為順序?qū)Ω黜検录M(jìn)行串聯(lián)并記錄完整的通信過程。通過該方式可將協(xié)議系統(tǒng)中的異常行為定位到具體環(huán)節(jié)。為避免舊消息的重放攻擊，協(xié)議系統(tǒng)要求用戶產(chǎn)生一個新的隨機(jī)值。past trace 集合形式化表示為在跟隨事件trace 時涉及的所有項目。past 函數(shù)通過直接遞歸定義，事件跟隨則是一個信息不斷積累的過程。

在攻擊者特有的操作函數(shù)基礎(chǔ)上進(jìn)一步構(gòu)造一個面向所有用戶的ptl_master 函數(shù)，使用該函數(shù)可形式化表示用戶的知識。與誠實用戶相比，攻擊者掌握的信息更應(yīng)受到關(guān)注，Attacker ptl_master trace 語句表示在跟隨事件trace 時攻擊者可用信息的集合。攻擊者早在消息交互前就開始處理一些舊的加密消息，在獲得被害用戶私鑰的前提下，對于通信過程中出現(xiàn)的所有以該用戶密鑰加密的消息，攻擊者都可以直接解密并竊取消息內(nèi)容。集合ptl_analyse（ptl_master Attacker trace）表示在跟隨事件的過程中攻擊者對于事件trace 中涉及的信息進(jìn)行分析得到的知識集合。集合ptl_create（ptl_analyse（ptl_master Attacker trace））表示知識生成的虛假信息集。

3.5 協(xié)議流程建模

在協(xié)議流程形式化表示的過程中，對于用戶代理發(fā)送的消息序列采用規(guī)則歸納方式進(jìn)行建模，具體過程如下：

inductive_set D_protocol：："trace list set"

where

Null："［］∈D_protocol"

| False："［| M∈ptl_create（ptl_analyse（ptl_master Attacker tracef））；tracef∈D_protocol；|］?Send Attacker B M # tracef∈D_protocol"

|MSG1："［|Random RA？past trace1；trace1∈D_protocol；|］?Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝#trace1∈D_protocol）"

|MSG2："［|Send A'B（Encrypt（mapPu_Key B）［Random RA，Define A］）∈set trace2；

trace2∈D_protocol；Random RA？past trace2|］?Send B A（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］｝）# trace2∈D_protocol"

|MSG3："［|Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝）∈set trace3；

Send B A'（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］｝）∈set trace3；

trace3∈D_protocol；Random r ？past trace3|］?Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）# trace3∈D_protocol"

|MSG4："［|Send A B（Encrypt（mapPu_Key B）｛［Random RA，Define A］｝）∈set trace4；

Send B A（Encrypt（mapPu_Key A）｛［Random RA，NonceK B，Define B］））∈set trace4；

Send A'B（Encrypt（NonceK B）｛［Random r，Define A］｝）∈set trace4；trace4∈D_protocol|］?

Send B A（Encrypt（NonceK B）｛［Random r］｝）# trace4∈D_protocol

除了Null 規(guī)則和False 規(guī)則之外，以上形式化建模的具體步驟都是按照消息序列的歸納定義而來。Null 規(guī)則引入了空追蹤，是歸納證明的第1 步操作，F(xiàn)alse 規(guī)則模擬攻擊者構(gòu)造欺詐消息的行為。通信協(xié)議入侵者采用重放攻擊的策略，將上一階段通信過程中的有利信息用于此次的攻擊操作。

從語義方面解釋MSG3 規(guī)則，與其對應(yīng)的半形式化語句如下：

Tom →Dick：Temkey { random，Tom }

MSG3 規(guī)則中涉及的第1 個Send 事件表示A 用戶向B 用戶發(fā)送的第1 條消息已經(jīng)加入第3 步事件跟隨中。該規(guī)則中涉及的第2 個Send 事件則表示B 用戶向另一方回復(fù)第2 條消息，用以確定通信另一方用戶A 的身份。上述兩個事件在第3 步事件跟隨前已經(jīng)發(fā)生。分析MSG3 規(guī)則中的第3 步操作：

Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）# trace3 ∈D_protocol

該操作是MSG3 規(guī)則的一項擴(kuò)充事件，其作為用戶身份信息的補(bǔ)充說明，并以新密鑰加密隨機(jī)值，在正式通信之前再次握手，確認(rèn)雙方身份。

在通信過程中，每新增一條消息則需要將其加入到事件軌跡中，更新跟隨狀態(tài)。當(dāng)通信過程受到入侵時，可以很容易將入侵行為定位到具體的消息步驟進(jìn)而對其進(jìn)行分析。以上形式化過程的語義模型主要基于Isabelle/HOL 中的集合論，將歸納分析方法作為形式化策略，將非正式的半形式化表達(dá)式轉(zhuǎn)化為正式的形式化模型。

4 通信協(xié)議安全性證明

4.1 相關(guān)定理證明

根據(jù)通信協(xié)議規(guī)范，誠實用戶代理總會生成新的隨機(jī)值說明當(dāng)前消息的時效性，在一次通信過程中雙方代理生成相同隨機(jī)數(shù)的概率幾乎為0，只有攻擊者才會試圖以舊的隨機(jī)值欺騙用戶，因為其不知道該隨機(jī)值的特殊性。通過定理1 說明通信過程中雙方代理生成的隨機(jī)值互不相同。

定理1

lemma unlike_random：

"［|trace ∈D_protocol；

Encrypt（mapPu_Key E）｛［Random RA，Define A］｝∈ptl_piece（ptl_master Attacker trace）；

Encrypt（mapPu_Key F）｛［RA'，Random RA，Define C］｝∈ptl_piece（ptl_master Attacker trace）|］?

Random RA ∈ptl_analyse（ptl_master Attacker trace）"

驗證過程如下：

apply（erule rev_mp，erule rev_mp）

apply（simp_all）

apply clarify

apply（erule D_protocol.induct）

apply（auto）

apply（simp add：ptl_analyse_insertI）

apply（blast intro：ptl_analyse_conjE）+

done

在定理1 的基礎(chǔ)上，提出與隨機(jī)值相關(guān)的定理2。在一次通信過程中，如果兩條消息的結(jié)構(gòu)相同且消息包含的隨機(jī)值不被入侵者掌握，則可以確定這兩條加密消息完全相同。

定理2

lemma："［|trace ∈D_protocol；Random ra ?ptl_analyse（ptl_master Attacker trace）；

Encrypt（NonceK agy）｛［Random ra，Define agx］｝∈ptl_piece（ptl_master Attacker trace）；

Encrypt（NonceK agy'）（Random ra，Define agx'）∈ptl_piece（ptl_master Attacker trace）|］?

agx=agx'?agy=agy'"

如果用戶生成的隨機(jī)數(shù)或者其私鑰被攻擊者竊取，則該用戶參與的通信過程很容易受到入侵，此時需要將其納入被害用戶集合victim_Muster。反之，如果用戶的隨機(jī)數(shù)和密鑰均為保密，則該用戶不在victim_Muster 集合中。根據(jù)以上描述，提出并驗證安全性定理3。

定理3

lemma secure_user：

"［|trace ∈D_protocol；

（Form（mapPr_Key C）∈ptl_piece（ptl_master Attacker trace））；

Random C ∈ptl_analyse（ptl_master Attacker trace）|］?C ∈victim_Muster"

驗證過程如下：

apply ptl_master_aux

apply（drule mp，assumption）+

apply（erule D_protocol.induct）

apply（erule conjE）

apply（auto）

done

4.2 安全性證明

如果通信協(xié)議雙方都為安全，則其交互的信息必然不會被攻擊者竊取，隨機(jī)生成的密鑰值為絕對安全，且后續(xù)通信過程也不會遭受攻擊。以通信協(xié)議的第2條消息為例，通過定理4 證明密鑰的保密性。

定理4

lemma Key_Secret［simp］：

"［|trace ∈D_protocol；

T ?victim_Muster；D ?victim_Muster；

Send T D（Encrypt（mapPu_Key D）｛［Random RT，NonceK T，Define T］｝）∈set trace |］?

NonceK T ?ptl_piece（ptl_master Attacker trace）"

驗證過程如下：

apply（simp_all）

apply（insert D_protocol_victim_aux）

apply（force simp add：protocol_secret_pros）

apply（erule D_protocol.induct）

apply（auto）

done

D_protocol 協(xié)議流程建模的主要目的是為建立代理用戶的通信，確保雙方身份的真實性。用戶A向用戶B 發(fā)送一條消息，并且用戶B 的反饋消息內(nèi)容符合協(xié)議規(guī)范，則可確定用戶A 身份的真實性。由于用戶A 和用戶B 均不屬于被害人集合，因此加密消息體將保持絕對安全，并且此后的通信過程可避免隨機(jī)值重放攻擊現(xiàn)象的發(fā)生。為提高協(xié)議流程的整體安全性，提出安全性定理5。

定理5

Theorembelief："［|trace ∈D_protocol；

A ?victim_Muster；B ?victim_Muster；

Send A B（Encrypt（NonceK B）｛［Random r，Define A］｝）∈set trace；

Send B' A（Encrypt（NonceK B）｛［Random r］｝）∈set trace |］?（Random r ? ptl_analyse（ptl_master Attacker trace））?（Send B A（Encrypt（NonceK B）｛［Random r］｝）∈D_protocol）"

定理5 在Isabelle/HOL 中的驗證過程與結(jié)果如圖3 所示，No subgoals 表明驗證完成且未產(chǎn)生新的待證子目標(biāo)。

圖3 Isabelle/HOL 驗證過程與結(jié)果Fig.3 Verification process and result of Isabelle/HOL

5 結(jié)束語

Isabelle/HOL 作為一種功能全面的定理證明輔助工具，在確保驗證過程正確性的同時可以提高驗證效率，并被廣泛應(yīng)用于各種安全性驗證研究工作中。本文借助Isabelle/HOL驗證了新構(gòu)造的D_protocol協(xié)議的安全性，在對協(xié)議流程進(jìn)行形式化建模的基礎(chǔ)上，采用歸納分析方式對消息交互過程涉及的相關(guān)性質(zhì)展開驗證，結(jié)果顯示D_protocol 協(xié)議具有抵抗外部攻擊能力的同時可以規(guī)避中間人欺騙行為的發(fā)生。另外，本文使用Isabelle/HOL 對用戶對象進(jìn)行形式化建模并采用函數(shù)語義模型抽象描述用戶行為，展示了其在驗證通信協(xié)議性能方面的應(yīng)用，并且可為其他領(lǐng)域的形式化驗證研究提供理論依據(jù)。然而，由于本文使用的定理證明方法主要在數(shù)理邏輯層面驗證系統(tǒng)相關(guān)性質(zhì)的正確性，但數(shù)量有限的定理無法描述無限的系統(tǒng)狀態(tài)，因此驗證結(jié)論在一定程度上是不完備的。下一步將結(jié)合定理證明和模型檢測兩種形式化分析方法檢查通信協(xié)議漏洞并驗證相關(guān)性質(zhì)的正確性，從而更全面地分析并研究通信原型系統(tǒng)的安全性。