基于安全協議代碼的形式化輔助建模研究

作者簡介：葛藝（1998－），女，安徽合肥人，碩士，主要研究方向為信息安全；黃文超（1982－），男（通信作者），湖北宜昌人，副教授，碩導，主要研究方向為網絡安全、形式化驗證等（huangwc@ustc.edu.cn）；熊焰（1960－），男，安徽宿松人，教授，博導，主要研究方向為計算機網絡與信息安全、移動計算等．

摘 要：隨著安全協議形式化分析技術的不斷發展，利用工具自動驗證雖已得到實現，但建模環節仍需依賴專業人員手工建模，難度大且成本高，限制了此技術的進一步推廣。為了提高建模的自動化程度，提出了依據安全協議代碼進行形式化模型輔助生成的方案。首先，使用污點分析獲取協議的通信流程，并且記錄密碼學原語操作；然后，根據通信流程之間的序列關系構建協議通信狀態機；最終，根據目前主流的安全協議形式化分析工具Tamarin的模型語法生成形式化模型。實驗結果表明，此方案可以生成形式化模型中的關鍵部分，提高了形式化建模的自動化程度，為形式化分析技術的推廣作出貢獻。

關鍵詞：形式化驗證；形式化建模；協議代碼；污點分析；Tamarin

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

文章編號：1001－3695（2023）04－037－1189－05

doi：10.19734/j.issn.1001-3695.2022.08.0446

Abstract：With the development of formal analysis technology of security protocols，automatic verification using tools has been realized，but modeling still needs to rely on manual modeling by professionals，which is difficult and costly and limits the further spread of formal analysis technology.In order to improve the automation of formal modeling，this paper proposed a scheme of formal assistant modeling based on security protocol code.Firstly，the method used taint analysis to obtain communication processes and record the cryptographic primitive operations.Then，it constructed the protocol communication state machine according to the sequential relationship between communication processes.Finally，it generated a formal model according to the syntax of Tamarin，a mainstream formal analysis tool for security protocols.Experimental results show that this scheme can gene-rate the key parts of the formal model and improves the degree of automation of the formal modeling，which contributes to the spread of formal analysis technology.

Key words：formal verification；formal modeling；protocol code；taint analysis；Tamarin

0 引言

安全協議是以密碼學為基礎的信息交換協議，為計算機系統中的信息安全提供了基礎保障。然而，安全協議的運行環境通常是不安全的，協議的設計一旦存在缺陷，就會造成不可挽回的后果。為了避免這種情況的發生，需要盡早地對協議進行安全性驗證。安全性驗證包括人工審查以及形式化驗證，人工審查的效率較低且準確性不高，相比之下，形式化驗證通過更加正規、嚴謹的方法對安全協議進行驗證，找出協議中存在的漏洞，對協議的設計起到重要的指導作用。

早在1996年，文獻[1]就利用形式化分析發現了NSPK協議的中間人攻擊。隨后，研究者們開發并使用形式化分析工具分析了大量安全協議，比如AVISPA工具針對IKEv2協議、H.530協議以及ISO-PK協議進行了形式化分析并且發現了相關攻擊[2～4]；Scyther對IKE協議族進行了分析，發現了IKEv1和IKEv2協議的并行攻擊[5]。利用形式化驗證工具對安全協議進行分析是一種準確高效的方式，以相應的形式化模型為輸入，通過工具進行邏輯推理，最后輸出驗證結果。近十年來，安全協議的形式化驗證研究取得了顯著進展，目前主流的形式化驗證工具（如Prove-rif[6]、AVISPA[7]、Tamarin-prover[8]、Scyther[9]等）可以在幾秒鐘內自動驗證Kerberos V或TLS握手等經典協議模型的機密性和身份驗證屬性，對無數個會話進行驗證，其中Tamarin-prover擁有較豐富的表達能力，常被用于安全協議分析。

安全協議的形式化驗證包含建模和驗證兩個主要步驟，建模階段構建形式化模型，在驗證階段對其進行驗證得到最終的驗證結果。目前，已經有研究實現了驗證步驟的全自動化[10]，但是在建模階段仍然是以手工建模為主。形式化建模以協議描述為依據提取出安全協議描述，協議描述可以是協議規范或者協議代碼，人工建模通常選取可讀性更高的協議規范作為依據，復雜安全協議的規范說明長達上百頁，包括嚴格的協議機制說明、隱式的安全保障以及介紹性文字，這要求建模人員擁有較高的專業技能，是一項非常繁重的工作。此外，由于各形式化驗證工具對模型要求的差異，形式化模型的通用性往往很低，限制了形式化分析技術的推廣。除了完全依賴人工建模以外，還有一部分輔助建模的工作，Cremers等人[11]利用Tamarin對TLS1.3協議進行了形式化分析，在建模時不是將協議規范直接轉換成Tamarin協議模型，而是利用m4預處理器定義了大量的宏，可以覆蓋協議規范的大部分，同時在語法上接近Tamarin模型語言，以這種方式構造模型可以實現與協議規范的直接比較，同時可以根據需求靈活修改。盡管這在一定程度上提高了模型的靈活性，但是仍然偏向手工建模，需要大量專家的參與，沒有從根本上解決形式化建模的痛點。

與協議規范不同，協議代碼作為安全協議的實現方式，往往由高級程序語言編寫而成，不但有著嚴格的語法并且包含了代碼實現的底層操作以及邏輯層面的協議流程，在嚴格遵循協議規范的情況之下，實現了協議流程中的所有步驟，對其進行自動的形式化建模可以輔助安全協議的形式化驗證分析，為研究人員提供了另一種建模參考和思路，減輕了人工建模的負擔，降低了形式化驗證技術的門檻。Stephens等人[12]通過將智能合約以及要滿足的安全屬性轉換成Buchi自動機來進行驗證，然而智能合約的代碼比較簡單，相較于用復雜編程語言實現的安全協議代碼，對其進行自動轉換較好實現。對于復雜的編程語言，文獻[13]將安全協議的Web實現轉換為應用Pi演算模型，半自動地完成了從協議代碼到驗證模型的轉換，但是此工作僅適用于Python編寫的協議實代碼。文獻[14]則是將函數調用抽象為函數調用時序圖，并基于靜態執行下的函數調用序列，給出了C程序中函數調用在Pi演算模型中的抽象方法，但是所選取的形式化驗證工具限制了工具適用的范圍。除此之外，還有一部分工作直接對安全協議代碼進行建模，將程序代碼轉換為計算模型[15]、Petri網[16]模型等，盡管這些工作可以實現從代碼到模型的自動轉換，但是只能夠針對代碼的底層漏洞進行檢測，并不能夠檢測到代碼里的協議邏輯漏洞。

從協議代碼到形式化模型的轉換本質上是對協議代碼進行抽象的過程，需要采用一種中間形式來完成這樣一種轉換，而代碼的運行過程與形式化模型的推理過程都可以被視為狀態機的轉換過程，所以本文采用了狀態機作為中間轉換形式，由于此狀態機包含的內容是協議通信的過程，稱之為通信狀態機。從協議代碼到通信狀態機的轉換實際上是對代碼進行信息提取，提取出與建模相關的關鍵信息，即協議的通信流程，采用程序分析中的數據流跟蹤，而從通信狀態機到形式化模型的轉換需要根據具體的形式化驗證工具的模型語言來制定具體的轉換規則。綜上，本文提出了一種基于污點分析的模型生成方法，整體框架如圖1所示。首先，利用污點分析方法提取協議代碼中的通信流程信息，并且記錄消息經過的密碼學原語操作，然后根據協議通信流程之間的序列關系構建通信狀態機，最后依據形式化模型的語法，將狀態機的狀態轉移邊轉換為對應的形式化模型語句，自動化地完成形式化建模，減輕人工負擔，降低學習成本，推進形式化分析技術的發展。

1 基本理論

1.1 污點分析

污點分析是程序數據流分析的一個典型應用[17]。當存儲在x中的數據被傳入y時，就產生了從x流向y的數據流，記做x-gt;y[1]。在污點分析中，當一個變量v的來源是未知的或者不被信任的，它將帶有污點標記，稱為被污染的（tainted）數據，如果對這個變量進行操作op獲得一個返回值rt，根據這個返回值是否也會變為被污染的數據，可以將操作（op）分為兩類。如果rt經過op后也變為了污點數據，那么op被稱為傳播操作，反之，op稱為過濾操作。其中，傳播操作具有傳遞性，也就是說，如果帶有污點標記的變量x通過操作op得到y，y又通過操作op得到z，則產生了一條污點傳播路徑x→z。

污染分析的API由以下四組操作組合而成，直觀過程如圖2所示。

a）sources，即污點源，代表可以生成污染數據的操作集。

b）propagators，即傳播操作，表示傳播或轉換污染數據的操作集。編程語言中的復制操作，比如賦值和參數傳遞，都被認為是傳播操作，如果存在指針或者引言，還要考慮別名現象。

c）filters，即過濾操作，是從污染數據生成安全數據的操作集。

d）sinks，即匯聚點，是一組用于判斷是否使用了污點數據的操作集，此類操作是需要重點關注的。

1.2 Tamarin模型

Tamarin基于多重集合改寫規則描述協議流程，利用一階邏輯量化協議消息和時間節點，從而實現對協議屬性的描述，支持具有復雜控制流的協議或者具有非單調易變全局狀態的協議，支持eCK等強安全模型，支持多種代數性質：加/解密運算、運算結合律、Diffie-Hellman冪運算以及雙線性對運算，它是目前主流的針對安全協議的形式化驗證工具，被廣泛地應用于各類安全協議的分析。Tamarin的輸入即為Tamarin模型，被定義在spthy文件中，通過重寫規則指定協議中不同角色的行為。這些重寫規則定義了有標記的轉換系統，它的狀態包括對手的知識、網絡消息、協議狀態等。Tamarin使用方程式理論來支持常見的密碼原語，如加密和哈希，并且使用跟蹤屬性對安全屬性進行建模。下面對Tamarin模型中兩個重要的組成部分進行簡單的介紹：

a）規則（rules）。一條重寫規則包含規則的名字以及三個部分，每一個部分都是事實（facts）的集合，分別稱為前提（premise）、動作（action）和結論（result）。規則的名稱僅用于引用特定的規則。它們沒有特定的含義，可以任意選擇，只要每個規則都有一個唯一的名稱即可，如果一個規則沒有被action事實標記，那么箭頭符號--[]-gt;可以縮寫為--gt;。轉移系統的初始狀態為空的多重集合，規則定義了系統如何向新狀態進行轉移。如果一個規則可以實例化（規則左側包含在當前狀態下），則可以將該規則應用于該狀態。在這種情況下，左側的事實被從狀態中移除，并被右側實例化所取代。比如，針對以下的這條規則，名字為rule_example，前提為[fact1，fact2]，當前提得到滿足時，應用這條規則可以得到[fact3，fact4]。

（a） in事實。用于建模在Dolev-Yao攻擊者控制的不可信網絡上接收消息的行為，并且只能發生在重寫規則的左側。

（b） out事實。用于建模在Dolev-Yao攻擊者控制的不可信網絡上發送消息的行為，并且只能發生在重寫規則的右側。

（c） Fr事實。當需要生成新變量時，必須使用這個事實，并且只能發生在重寫規則的左側，其中它的參數是新的項，可以用于建模產生隨機值的行為。

2 基于污點分析的信息提取

信息提取模塊包含消息傳遞流程提取以及密碼學原語提取兩個部分。消息傳遞流程即協議參與方之間收發消息的流程，是形式化模型中的主要組成部分，消息傳遞流程提取作為自動化建模的第一步，為構建形式化模型整體框架奠定了基礎。密碼學原語則為不需要展開分析的密碼學操作函數，在形式化模型中用于描述消息所經過的密碼學操作，進行密碼學原語提取是為構建更加精細的形式化模型。本工作通過污點分析跟蹤協議代碼中的收發消息的API來獲取消息傳遞流程，與此同時，在跟蹤收發消息流程時，記錄消息經過的密碼學原語。在后續建模時，依據信息提取模塊獲得的信息對安全協議流程以及消息經過的密碼學原語進行描述。

2.1 消息傳遞流程提取

消息傳遞流程是指協議參與方之間傳遞消息的步驟，包括發送方、接收方以及參與方之間傳遞的消息，多條消息傳遞流程共同組成了安全協議的通信流程。在用形式化模型對安全協議進行描述時，主體框架即為消息傳遞流程，因此，首先需要通過分析協議代碼獲取消息傳遞流程。

本文方案利用污點分析技術提取安全協議代碼中的收發消息數據流。首先，將收發消息數據流提取映射到污點分析的情形之下，將接收消息的API作為source，發送消息的API作為sink，可以用如圖3所示的有限狀態機來描述，對應的五元組為（Q，P，δ，q0，F），其中：

獲取的一條污點分析路徑，代表著一次消息收發過程，具體包含了消息來源方、消息接收方以及傳遞的消息變量，此處將這些信息記錄下來以備后續使用。

2.2 密碼學原語提取

消息傳遞流程中的消息一般都會經過一系列的密碼學操作，即密碼學原語，為了在形式化模型中對其進行更加精準的描述，在跟蹤收發消息數據流的同時，記錄消息經過的一系列密碼學原語。

在協議代碼中，密碼學操作往往由函數來實現，在密碼學函數中包含了代碼實現的具體細節，例如，下面的函數表示加密操作，包含了加密算法的具體實施以及錯誤判斷。由于在構建形式化模型時采取完美密碼理論，可以忽略密碼學操作的具體實現，將密碼學函數作為黑盒處理，只關注函數的密碼學功能，而不關注具體的密碼學算法。所以，以上的函數直接抽象為加密原語enc。

int encrypt（void*buffer，int buffer_len，char*IV，char*key，int key_len）

{

MCRYPT td=mcrypt_module_open（\"rijndael-128\"，NULL，\"cbc\"，NULL）；

int blocksize = mcrypt_enc_get_block_size（td）；

if（buffer_len % blocksize！=0）{return 1；}

mcrypt_generic_init（td，key，key_len，IV）；

mcrypt_generic（td，buffer，buffer_len）；

mcrypt_generic_deinit（td）；

mcrypt_module_close（td）；

return 0；

}

在本文中關注兩類密碼學原語，即加密原語和解密原語。

定義1 密碼學原語序列CryOpt（op1，op2，…），op為解密原語或者加密原語，加密原語和解密原語分別用enc和dec表示。

類似source和sink的設置，在污點分析開始之前，根據代碼預先設置好加/解密原語的API，在進行污點分析的同時，記錄經過的密碼學操作，組成密碼學原語序列CryOpt。

3 協議通信狀態機構建

通過污點分析獲取到消息傳遞流程之后，為了表示這些消息傳遞流程之間的序列關系，構建了安全協議的通信狀態機，作為協議源代碼向形式化模型轉換的中間表示形式。針對每一條消息傳遞流程，發送的消息往往取決于接收的消息，根據這個特點，本文方案采取米利狀態機（Mealy machine）的結構。

米利狀態機是基于當前狀態和輸入生成輸出的有限狀態自動機，它的狀態圖的每個轉移邊包括輸入和輸出，一個Mealy machine由一個六元組（S，I，O，δ，X，s0）表示，其中S是一個狀態的有限集，I是輸入的有限集，O是輸出的有限集，δ是狀態的轉換關系集合S×I→S，X是輸出的轉換關系集合S×I→O，s0是初始狀態，且s0∈S；δ中的一個轉換關系sk×ik→sk+1表示從當前狀態sk出發，接收輸入ik后，狀態轉換為sk+1；X中的一個轉換關系sk×ik→ok表示從當前狀態sk出發，接收輸入ik后，輸出為ok；其中，sk∈S，sk+1∈S，ik∈I，ok∈O。Mealy machine的輸出取決于當前狀態和當前輸入，

從初始狀態出發，給定一個輸入序列，狀態轉換序列和輸出序列也是確定的。因此，當初始狀態給定的情況下，可以用Mealy machine中從初始狀態s0出發到某一目標狀態st的所有輸入序列集合來表示狀態的信息，這是將協議實現的Mealy machine抽象信息用于指導形式化建模的理論基礎。

基于已經得到的污點分析路徑，本文設計了協議的狀態機構建算法。每個協議參與方R都擁有唯一標識符ID，根據污點路徑出現的先后順序為每個協議參與方R生成通信流程R.Seq，每一條污點路徑作為通信流程序列中的一個元素，表示一次收發消息操作，包括消息來源方、消息接收方、消息以及消息經過的密碼學原語，將通信流程序列定義如下：

定義2 每一個協議參與方R包含唯一標識符ID和通信流程隊列Seq，其中，通信流程序列R.Seq，R.Seq[i]表示第i條污點路徑包含的信息，可以展開為（from，to，mes，dec，enc），其中from表示消息來源方，to表示消息接收方，mes表示發送的消息變量，dec表示解密原語的次數，enc表示加密原語的次數。

協議通信狀態機構建的具體流程如算法1所示。首先，指定協議發起方S并且配置初始通信信息V0，包括初始消息的接收方以及經過的密碼學原語，將V0作為狀態機的初始狀態節點。然后，到當前參與方curNode的消息接收方curRule的通信流程序列中獲取頭節點，作為curNode節點對應狀態的下一個狀態，直到所有的參與方的通信流程序列皆被遍歷，算法結束，返回狀態機M。

4 形式化模型生成

本文所選取的形式化驗證工具Tamarin對應的形式化模型被定義在.spthy文件中，包含幾個組成部分：協議流程模型、攻擊者模型以及安全屬性。由于本文只關注協議本身的建模，所以攻擊者模型以及安全屬性不在考慮范圍內。協議流程模型由多條規則（rules）組成，每一條規則擁有唯一的規則名稱，包含前提、動作和結論三個部分，每一個部分都是事實（facts）的集合，下面詳細描述從通信狀態機到具體規則的轉換方式。

5 實驗案例與分析

5.1 實驗設計與實現

目前已有的利用協議代碼自動建模的方案并不多，并且都關注于形式化驗證的結果[11，15]，并沒有對生成的形式化模型做過多的分析，而本文關注于模型生成的過程與質量；另外，針對同一個協議最終構建的形式化模型并不是唯一的，有多種描述方式。基于以上原因，本文的實驗結果難以與其他自動建模方案進行橫向或縱向的對比。由于缺少同類方法的比較，本文設計了五個指標量化了模型的生成效果，也將此作為后續工作改進的基準。

在分析實驗結果時，為了驗證污點分析提取協議流程信息的準確性，需要對所有的污點路徑進行人工分析，將每一條污點路徑與協議流程進行匹配，對匹配結果進行分析。其次，為了驗證整體方案的有效性，采取將生成的模型與手工建模的模型進行對比的方式，從以下幾個維度進行分析，其中手工建模的模型采用的是Tamarin官方案例中提供的形式化模型：

a）規則個數（NR），一個形式化模型文件中所有規則（rules）的個數。

b）in事實個數（NI），所有rules中in事實的個數。

c）out事實個數（NO），所有rules中out事實的個數。

d）參數個數（NP），所有事實中包含的參數的個數。

e）密碼學原語個數（NC），所有事實中包含的加/解密操作的個數。

以上五個指數越接近，表示生成的模型與手工建模的模型相似性越高，因此通過計算兩者的百分比可以直觀地表示出模型的相似性，由于官方提供的手工建模模型已經被實際檢驗過，可以認為相似性越高，方案的有效性就越高。

本文選取的安全協議代碼為C語言實現，系統內置了代表接收和發送消息的函數作為source和sink，另外用戶也可以根據需求自行定義，source和sink作為配置文件與協議C代碼共同作為系統的輸入，在進行污點分析時采用clang-4作為后端，利用clang static analyzer提供的接口實現用戶可配置的污點分析，然后將結果作為算法1的輸入得到通信狀態機，最后根據模型生成規則得到形式化模型。

實現過程可分為以下幾個步驟：

a）將source和sink作為配置文件，與協議C代碼輸入到系統中；

b）污點分析器讀取配置文件，根據source和sink分析協議C代碼，返回污點分析路徑；

c）指定協議參與方集合role，協議發起方S以及初始通信信息V0，根據算法1計算通信狀態機；

d）根據第4章的轉換規則，將通信狀態機轉換為Tamarin模型。

5.2 案例分析

Needham-Schroeder協議（NS協議）是一個基于對稱加密算法的協議，它要求有可信任的第三方 KDC 參與，采用challenge/response 的方式，使得A、B互相認證對方的身份。A是協議的發起者，B是協議的響應者，K是認證服務器，是A生成的隨機數，Nb是B生成的隨機數，Kab是S生成的會話密鑰，Kas是A和S的共享密鑰，Kbs是B和S的共享密鑰。在成功完成上述協議后，A和B就能確信他們之間擁有一個僅為他們和認證服務器知道的會話密鑰Kab，協議流程如下：

a）A-gt;K：A，B，Na

b）K-gt;A：{Na，B，Kab，{Kab，A}Kbs}Kas

c）A-gt;B：{Kab，A}Kbs

d）B-gt;A：{Nb}Kab

e）A-gt;B：{succ（Nb）}Kab

在進行污點分析時，如圖5所示，KDC.c文件中，recvfrom函數將污點標記賦給request結構體，然后request通過字符串拷貝操作將污點標記傳播給reply中的成員變量receiverHostname，在匯聚函數sendto中判斷第一個參數是否被污染，而第一個參數為reply結構體對象。

對于用于挖掘漏洞的污點分析而言，為了避免假陽性過高的問題，這種情況下并不會產生污點數據泄露報告，但是為了達到本文協議流程提取的目的，需要提高污點傳播的能力，當結構體成員變量被污染時認為結構體對象也是被污染的，從而產生污點數據泄露報告，對應一條協議流程路徑，如圖6所示。

其他規則的生成也采取類似的方法，規則生成的順序與通信狀態機的狀態轉移順序一致，下一條規則的in事實中包含的參數與上一條規則中out事實的參數一致，表示參與方之間的消息收發順序。

5.3 實驗結果與分析

通過以上的案例分析，得到了最終生成的形式化模型，對其進行進一步分析，目的在于驗證污點分析在此方案中的有效性以及評估生成的形式化模型的質量。

首先，對污點分析提取協議流程信息的正確性進行驗證，結果如表1所示。污點分析一共返回了四條污點路徑，經過比對，包含了協議流程中除發起步驟之外的所有步驟，對于發起步驟，由于其并沒有接收消息的前提，也就沒有接收消息的API可以作為污點源，所以無法通過污點分析得到，在后續的狀態機構建算法中通過事先指定協議發起方以及初始通信信息來補全這里的缺失。因此，污點分析對于本案例的有效性得到證實。

其次，將生成的NS協議的形式化模型與Tamarin中手工建模的模型進行對比，指標統計結果如表2所示。

從實驗結果可以看出，本文方案可以生成大多數的規則，經過分析，這些規則都與協議流程主體有關，這與污點分析提取協議流程的目的一致，其余兩條無法生成的規則是對攻擊者能力的描述以及初始化參數的設置，這些都不包含在協議代碼中，因此需要依賴協議代碼以外的信息完成建模。由于目前方法難以分析協議代碼中具體參數的含義，還無法對消息參數進行更細致的建模，在參數個數上與手工建模的模型差距較大。此外，通過分析代碼可以對加/解密操作進行較為準確的建模，但是由于手工建模時對參數的建模更加細致并且采取了約簡措施，所以在密碼學原語個數的指標上有所差異。實驗結果表明，通過本文方案生成的形式化模型與手工建模的模型有較高的相似度，可以對安全協議的主要流程進行描述，但在提高自動化程度的同時損失了一些建模中的精確度，這需要在后續的工作中繼續改進。

6 結束語

形式化方法在安全協議驗證中發揮著越來越重要的作用，自動化程度關系著形式化方法的進一步推廣，針對形式化建模自動化程度低的問題，本文提出一種依據安全協議代碼自動生成形式化模型的方法。使用污點分析方法以及狀態機構建算法，獲得了協議流程中的關鍵信息，構造出了符合Tamarin驗證工具規范的形式化模型。對NS協議進行了自動模型生成實驗，結果表明，此方法可以生成與手工建模的模型相似的形式化模型，但是精確度仍然達不到手工建模的程度。下一步可以對消息參數進行提取，建立消息之間的綁定關系，提高模型的精確度，同時，可以將此方法應用到更加復雜的安全協議代碼之上，提高此方法的擴展性，從而進一步實現安全協議的形式化自動建模。本文探討的是安全協議的形式化自動建模方案，實現全自動建模是最高目標，目前提出的方案可以實現輔助建模，在一定程度上減輕了人工建模的壓力，降低了形式化驗證的門檻。

參考文獻：

［1］Lowe G.Breaking and fixing the Needham-Schroeder public-key protocol using FDR[C]//Proc of International Workshop on Tools and Algorithms for the Construction and Analysis of Systems.Berlin：Sprin-ger，1996：147-166.

[2]Ziauddin S，Martin B.Formal analysis of ISO/IEC 9798-2 authentication standard using avispa[C]//Proc of the 8th Asia Joint Conference on Information Security.Piscataway，NJ：IEEE Press，2013：108-114.

[3]Islam S.Security analysis of LMAP using AVISPA[J].International Journal of Security and Networks，2014，9（1）：30－39.

[4]Vigano L.Automated security protocol analysis with the AVISPA tool[J].Electronic Notes in Theoretical Computer Science，2006，155：61－86.

[5]Cremers C.Key exchange in ipsec revisited：formal analysis of IKEV1 and IKEV2[C]// Proc of European Symposium on Research in Computer Security.Berlin：Springer，2011：315－334.

[6]Blanchet B，Cheval V，Cortier V.ProVerif with lemmas，induction，fast subsumption，and much more[C]//Proc of Symposium on Security and Privacy.Piscataway，NJ：IEEE Press，2022：69－86.

[7]Sharma S，Kaushik B，Rahmani M K I，et al.Cryptographic solution-based secure elliptic curve cryptography enabled radio frequency identification mutual authentication protocol for Internet of Vehicles[J].IEEE Access，2021，9：147114-147128.

[8]Basin D，Cremers C，Dreier J，et al.Tamarin：verification of large-scale，real-world，cryptographic protocols[J].IEEE Security amp; Privacy，2022，20（3）：24－32.

[9]Dewangan N K，Chandrakar P.Patient-centric token-based healthcare blockchain implementation using secure Internet of medical things[J/OL].IEEE Trans on Computational Social Systems.2022.http：//doi.org/10.1109/TCSS.2022.3194872.

[10]Xiong Yan，Su Cheng，Huang Wenchao，et al.SmartVerif：push the limit of automation capability of verifying security protocols by dyna-mic strategies[C]//Proc of the 29th USENIX Conference on Security Symposium.2020：253－270.

[11]Cremers C，Horvat M，Hoyland J，et al.A comprehensive symbolic analysis of TLS 1.3[C]//Proc of ACM SIGSAC Conference on Computer and Communications Security.New York：ACM Press，2017：1773-1788.

[12]Stephens J，Ferles K，Mariano B，et al.SmartPulse：automated checking of temporal properties in smart contracts[C]//Proc of IEEE Symposium on Security and Privacy.Piscataway，NJ：IEEE Press，2021：555－571.

[13]He Xudong，Liu Qin，Chen Shuang，et al.Analyzing security protocol Web implementations based on model extraction with applied Pi calculus[J].IEEE Access，2020，8：26623－26636.

[14]張協力，祝躍飛，顧純祥，等.C2P：基于Pi演算的協議C代碼形式化抽象方法和工具[J].軟件學報，2021，32（6）：1581-1596.（Zhang Xieli，Zhu Yuefei，Gu Chunxiang，et al.C2P：formal abstraction method and tool for C protocol code based on Pi calculus[J].Journal of Software，2021，32（6）：1581-1596.）

[15]Aizatulin M，Gordon A D，Jyurjens J.Computational verification of C protocol implementations by symbolic execution[C]//Proc of ACM Conference on Computer and Communications Security.New York：ACM Press，2012：712-723.

[16]Petrosyan G R，Ter-Vardanyan L A.Modelling of identification and secret-key generation system with colored Petri net[C]//Proc of International Conference on Control，Decision and Information Technologies.Piscataway，NJ：IEEE Press，2016：239－245.

[17]劉嘉勇，韓家璇，黃誠.源代碼漏洞靜態分析技術[J].信息安全學報，2022，7（4）：100-113.（Liu Jiayong，Han Jiaxuan，Huang Cheng.Vulnerability detection in source code using statice analysis[J].Journal of Cyber Security，2022，7（4）：100-113.）