一種基于Isabelle/HOL 的安全通信協議驗證方法

夏 銳，錢振江，2，劉 葦

（1.蘇州大學 計算機科學與技術學院，江蘇 蘇州 215000；2.常熟理工學院 計算機科學與工程學院，江蘇 常熟 215500；3.國網電力科學研究院，南京 211000）

0 概述

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

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

1 相關工作

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

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

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

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

2 通信協議

2.1 協議簡介

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

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

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

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

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

2.2 協議內容

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

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

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

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

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

2.3 協議安全性分析

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

3 通信協議的形式化建模

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

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

Isabelle/HOL 是基于高階邏輯的形式化證明系統，被廣泛應用于計算機軟硬件模塊的可靠性證明及數學定理的安全性驗證等任務中［5，22］。Isabelle/HOL 具有強大的對象描述能力和程序規約表達能力，可以借助類型系統與邏輯之間的同構關系，將定理證明的過程轉變為程序編寫的過程。由于證明過程的正確性可以通過機器進行自動檢查，因此無須依靠自動定理證明算法的正確性，驗證結果更具說服力［23］。本文證明過程主要涉及Isabelle/HOL 的歸納集合論，通過定義不同的數據類型及成員函數對D_protocol 協議內容進行表達。

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

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

datatype ptl_agent=User|Attacker

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

type_synonym key=nat

consts mapK：："key?key"

通過定義ptl_msg 數據類型引入通信中消息的標準形式，標準消息包括由代理、密鑰、用戶生成的隨機值、復合消息及加密后的消息等信息，形式化表示如下：

datatype

ptl_msg=Define ptl_agent

Form key

Random nat

Couple ptl_msg ptl_msg

Encrypt key ptl_msg

以上消息類型中出現了Encrypt 加密函數，Encrypt 加密函數是單射函數。在指定加密函數的情況下，如果兩條密文消息相同，根據單射函數的性質，則可以確定這兩條密文消息對應的明文消息，并且其加密密鑰也相同。

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

consts mapPu_Key：："ptl_agent ?key"

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

consts NonceK：："ptl_agent ?key"

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

abbreviation mapPr_Key：："ptl_agent ?key"

where "mapPr_Key A ≡mapK（mapPu_Key A）"

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

datatype trace=Send ptl_agent ptl_agent ptl_message

3.3 攻擊者行為建模

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

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

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"

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

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

Analyse_ide：ptl_analyse(ptl_analyse M)=ptl_analyse M

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

3.4 事件跟隨建模

本文將D_protocol 協議的通信過程形式化為一個各項事件跟隨的集合，以時間為順序對各項事件進行串聯并記錄完整的通信過程。通過該方式可將協議系統中的異常行為定位到具體環節。為避免舊消息的重放攻擊，協議系統要求用戶產生一個新的隨機值。past trace 集合形式化表示為在跟隨事件trace 時涉及的所有項目。past 函數通過直接遞歸定義，事件跟隨則是一個信息不斷積累的過程。

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

3.5 協議流程建模

在協議流程形式化表示的過程中，對于用戶代理發送的消息序列采用規則歸納方式進行建模，具體過程如下：

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 規則和False 規則之外，以上形式化建模的具體步驟都是按照消息序列的歸納定義而來。Null 規則引入了空追蹤，是歸納證明的第1 步操作，False 規則模擬攻擊者構造欺詐消息的行為。通信協議入侵者采用重放攻擊的策略，將上一階段通信過程中的有利信息用于此次的攻擊操作。

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

Tom →Dick：Temkey { random，Tom }

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

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

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

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

4 通信協議安全性證明

4.1 相關定理證明

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

定理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 的基礎上，提出與隨機值相關的定理2。在一次通信過程中，如果兩條消息的結構相同且消息包含的隨機值不被入侵者掌握，則可以確定這兩條加密消息完全相同。

定理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'"

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

如果通信協議雙方都為安全，則其交互的信息必然不會被攻擊者竊取，隨機生成的密鑰值為絕對安全，且后續通信過程也不會遭受攻擊。以通信協議的第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 協議流程建模的主要目的是為建立代理用戶的通信，確保雙方身份的真實性。用戶A向用戶B 發送一條消息，并且用戶B 的反饋消息內容符合協議規范，則可確定用戶A 身份的真實性。由于用戶A 和用戶B 均不屬于被害人集合，因此加密消息體將保持絕對安全，并且此后的通信過程可避免隨機值重放攻擊現象的發生。為提高協議流程的整體安全性，提出安全性定理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 中的驗證過程與結果如圖3 所示，No subgoals 表明驗證完成且未產生新的待證子目標。

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

5 結束語

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