密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

內(nèi)容簡介

本書主要探討密碼協(xié)議實現(xiàn)（密碼協(xié)議程序源代碼）時的邏輯安全性，并以密

碼協(xié)議實現(xiàn)時的安全性為前提條件，設(shè)計了新的方案。本書引入了邏輯推理與規(guī)則

的安全證明，在分析方面，討論了密碼協(xié)議實現(xiàn)時的軌跡安全、快速判斷密碼協(xié)議

實現(xiàn)時導(dǎo)致的不安全原因、基于內(nèi)容安全的密碼協(xié)議代碼實現(xiàn)模型分析和密碼協(xié)議

實現(xiàn)時的側(cè)信道安全分析。在設(shè)計方面，討論了非簽名認(rèn)證的密鑰協(xié)商協(xié)議設(shè)計和

基于協(xié)議底層實現(xiàn)安全的密鑰協(xié)商協(xié)議。所有的方法都通過源代碼（C語言和Socket

通信編程）進行實驗分析，實驗結(jié)果符合預(yù)期要求。

本書可作為計算機科學(xué)與技術(shù)、網(wǎng)絡(luò)空間安全、數(shù)學(xué)與應(yīng)用數(shù)學(xué)等信息安全專

業(yè)本科生、研究生的學(xué)術(shù)性指導(dǎo)教材，也可供高等院校從事網(wǎng)絡(luò)空間安全研究的學(xué)

者以及其他領(lǐng)域?qū)π畔踩信d趣的愛好者作為參考資料之用。

圖書在版編目（CIP）數(shù)據(jù)

密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計/吳福生,李延斌

著.—北京：中國鐵道出版社有限公司,2022.7

ISBN978-7-113-29091-7

Ⅰ.①密…Ⅱ.①吳…②李…Ⅲ.①密碼協(xié)議-研究

Ⅳ.①TN918.1

中國版本圖書館CIP數(shù)據(jù)核字(2022)第071385號

書名：密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

MIMAXIEYISHIXIANDELUOJIANQUANFENXIYUSHEJI

作者：吳福生李延斌

責(zé)任編輯：荊波編輯部電話：（010）51873026郵箱：the-tradeoff@

封面設(shè)計：

責(zé)任校對：焦桂榮

責(zé)任印制：趙星辰

出版發(fā)行：中國鐵道出版社有限公司（100054，北京市西城區(qū)右安門西街8號）

印刷：北京富資園科技發(fā)展有限公司

版次：2022年7月第1版2022年7月第1次印刷

開本：787mm×1092mm1/16印張：12字?jǐn)?shù)：252千

書號：ISBN978-7-113-29091-7

定價：79.00元

版權(quán)所有侵權(quán)必究

凡購買鐵道版圖書，如有印制質(zhì)量問題，請與本社讀者服務(wù)部聯(lián)系調(diào)換。電話：（010）51873174

打擊盜版舉報電話：（010）63549461

前言

密碼協(xié)議實現(xiàn)的安全分析是屬于數(shù)學(xué)、計算機和密碼學(xué)等交叉學(xué)科的研究熱點之

一，該領(lǐng)域的研究背景不僅需要數(shù)學(xué)、密碼學(xué)以及計算機程序語言編程技術(shù)等，而且還

涉及邏輯、統(tǒng)計等學(xué)科的體系知識，這是一個多學(xué)科交叉的研究領(lǐng)域。

密碼協(xié)議實現(xiàn)涉及復(fù)雜環(huán)境和多學(xué)科知識融合，交叉學(xué)科研究前景廣闊，主要應(yīng)用

于密碼軟件實現(xiàn)的邏輯安全分析、軟件設(shè)計的邏輯缺陷分析、基于邏輯安全的密碼協(xié)議

設(shè)計與分析、系統(tǒng)實現(xiàn)的漏洞檢測與分析等網(wǎng)絡(luò)空間安全領(lǐng)域。

密碼算法是密碼技術(shù)的核心固件，是網(wǎng)絡(luò)空間安全的核心技術(shù)。在保護公共信道方

面，信息傳輸起到至關(guān)重要的作用。密碼協(xié)議的安全是建立在密碼算法安全基礎(chǔ)之上的，

但又不同于密碼算法。密碼協(xié)議至少存在兩個參與者，按照一定的規(guī)則交互式地交換信

息。雖然基于密碼技術(shù)的協(xié)議在互聯(lián)網(wǎng)上得到了廣泛的應(yīng)用，在網(wǎng)絡(luò)空間安全領(lǐng)域中作

出了巨大的貢獻，但是隨著密碼協(xié)議實現(xiàn)環(huán)境的復(fù)雜化以及協(xié)同化要求越來越高，網(wǎng)絡(luò)

攻擊事件頻頻發(fā)生，密碼協(xié)議的分析與設(shè)計面臨巨大挑戰(zhàn)。

基于密碼技術(shù)的密碼協(xié)議在理論上被證明是安全的，但是在其編碼成為軟件實現(xiàn)

時，并不一定是安全的，原因在于密碼協(xié)議在設(shè)計時并沒有考慮其實現(xiàn)時的安全性，以

及在設(shè)計時的邏輯安全。針對這種情況，本書把密碼協(xié)議實現(xiàn)時的安全性作為闡述重點，

主要討論密碼協(xié)議代碼實現(xiàn)時的安全性，并以此作為設(shè)計新密碼協(xié)議方案的前提條件；

在復(fù)雜環(huán)境下，引入數(shù)理邏輯規(guī)則與邏輯證明、π-演算的移動與交互理論等，設(shè)計新

的密碼協(xié)議方案，并對新的密碼協(xié)議實現(xiàn)時進行邏輯安全分析。

對讀者的要求

本書主要探討復(fù)雜環(huán)境下密碼協(xié)議實現(xiàn)時的安全性，分析密碼協(xié)議實現(xiàn)的安全性需

求，設(shè)計新的密碼方案等。所以在技術(shù)上對讀者有如下幾方面的要求：

（1）具備良好的數(shù)學(xué)基礎(chǔ)知識、現(xiàn)代密碼學(xué)基礎(chǔ)知識和數(shù)理邏輯知識，例如，離散

數(shù)學(xué)、數(shù)論、現(xiàn)代密碼基礎(chǔ)知識以及邏輯規(guī)則等；

（2）具備計算機程序語言編程能力，例如，C語言、C++語言以及匯編語言等；

（3）需掌握一定的計算機網(wǎng)絡(luò)知識與網(wǎng)絡(luò)編程技術(shù)，例如，TCP/IP基礎(chǔ)知識以及

基于Socket套接字編程技術(shù)；

（4）具備一定的漏洞分析能力、反匯編能力和相關(guān)工具的使用能力；例如，漏洞分析、

熟悉C/C++反匯編語言、工具olldbg使用等；

（5）掌握一定的大數(shù)據(jù)處理與分析技術(shù)，例如，數(shù)據(jù)挖掘、機器學(xué)習(xí)和統(tǒng)計分析等。

本書寫作思路

本書是在長期從事網(wǎng)絡(luò)空間安全教學(xué)與科研的基礎(chǔ)上寫成的，秉承著理論與實踐相

結(jié)合的寫作思路。

ii密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

首先，基于密碼學(xué)的困難數(shù)學(xué)問題對密碼協(xié)議代碼實現(xiàn)的安全性進行分析，以密碼

協(xié)議代碼實現(xiàn)時的安全因素作為前提條件，設(shè)計新的密碼協(xié)議或改進現(xiàn)有的密碼協(xié)議，

使新的密碼協(xié)議適用于對復(fù)雜環(huán)境下信息的安全保護。

其次，對提出或改進的新密碼協(xié)議進行源代碼分析，包括密碼協(xié)議代碼實現(xiàn)時的特

征和行為的邏輯安全分析。

最后，通過具體的密碼協(xié)議源代碼實現(xiàn)的實驗來證實新方案的可行性。

本書是一本學(xué)術(shù)專著，基本框架是理論與實踐的融合，其理論主要來自數(shù)學(xué)、π-

演算以及移動通信系統(tǒng)等，考慮密碼協(xié)議代碼實現(xiàn)時的安全因素，提出新的密碼協(xié)議實

現(xiàn)安全分析方案或設(shè)計新的密碼協(xié)議。

本書讀者

本書可作為信息安全、網(wǎng)絡(luò)空間安全以及計算機科學(xué)與技術(shù)專業(yè)的本科生、研究生

學(xué)習(xí)與學(xué)術(shù)研究的指導(dǎo)性教材，還可供在高等學(xué)校從事信息安全、密碼學(xué)與應(yīng)用密碼學(xué)、

網(wǎng)絡(luò)空間安全等研究的工作者，以及網(wǎng)絡(luò)空間安全愛好者學(xué)習(xí)參考之用。

作者團隊與感謝

本書第8章由李延斌編寫，其余章節(jié)由吳福生編寫，并由吳福生對全書統(tǒng)稿。

本書的出版得到了國家自然科學(xué)基金項目（No.62062019,62072247,62061007）和貴

州財經(jīng)大學(xué)學(xué)術(shù)專著出版專項資助。在寫作過程中，引用了大量的文獻，在此謹(jǐn)向這些

文獻的作者表示誠摯的謝意。

因筆者學(xué)術(shù)水平有限，書中難免會有不妥和錯誤之處，對此，懇請讀者的理解和批

評指正，并于此先致感謝之意。

衷心感謝博士生導(dǎo)師張煥國教授，感謝碩士生朱嘉杰、王雪梅的細(xì)心校對以及給予

指導(dǎo)、支持和幫助的所有領(lǐng)導(dǎo)、專家和同行，衷心感謝本書的每一位讀者。

吳福生李延斌

2022年5月

目錄

第1章緒論

1.1引言1

1.2關(guān)鍵技術(shù)3

1.3本書結(jié)構(gòu)介紹4

參考文獻5

第2章密碼協(xié)議實現(xiàn)安全的研究現(xiàn)狀

2.1代碼模型提取安全驗證分析9

2.1.1C語言模型提取分析9

2.1.2Java語言模型提取分析15

2.1.3F#語言模型提取分析16

2.2代碼自動生成安全驗證分析18

2.2.1基于編譯器代碼自動生成分析19

2.2.2基于Java語言代碼自動生成分析20

2.3基于操作語義安全驗證分析22

2.4密碼協(xié)議精化安全驗證分析27

2.4.1精化檢測工具協(xié)議分析27

2.4.2程序精化分析28

2.4.3信息流精化分析29

2.5本章小結(jié)30

參考文獻30

第3章非簽名認(rèn)證的密鑰協(xié)商協(xié)議設(shè)計

3.1新協(xié)議涉及的群同態(tài)基礎(chǔ)知識39

3.1.1群同態(tài)的基本定義39

3.1.2群同態(tài)的基本定理39

3.2整數(shù)乘法同態(tài)二叉樹的構(gòu)造與分析40

3.3整數(shù)乘法同態(tài)二叉樹的基本遍歷與性質(zhì)41

3.4整數(shù)乘法同態(tài)二叉樹的密鑰協(xié)商協(xié)議42

3.4.1構(gòu)造一棵葉子結(jié)點為素數(shù)的整數(shù)乘法同態(tài)二叉樹42

3.4.2整數(shù)乘法同態(tài)二叉樹密鑰協(xié)商協(xié)議具體步驟43

3.5協(xié)議安全分析44

ii密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

3.5.1一般安全性分析44

3.5.2隨機預(yù)言模型（RandomOracleModel）的可證明安全分析45

3.6新協(xié)議結(jié)構(gòu)的安全分析46

3.7新協(xié)議性能比較與實驗分析46

3.7.1新協(xié)議的二叉樹存儲與遍歷46

3.7.2新協(xié)議實現(xiàn)的實驗47

3.7.3參數(shù)n對網(wǎng)絡(luò)通信的影響50

3.8本章小結(jié)52

參考文獻52

第4章通過密碼協(xié)議在代碼級上實現(xiàn)時的軌跡行為是否異常來評估其

安全性

4.1相關(guān)研究工作55

4.2知識準(zhǔn)備56

4.2.1標(biāo)號遷移系統(tǒng)與強模擬56

4.2.2程序的精化57

4.2.3密碼協(xié)議源代碼的程序精化58

4.3建立模型58

4.3.1密碼協(xié)議的符號化描述59

4.3.2密碼協(xié)議源代碼精化59

4.3.3程序控制流圖63

4.3.4從控制流圖到狀態(tài)圖65

4.3.5密碼協(xié)議實現(xiàn)的軌跡65

4.4密碼協(xié)議實現(xiàn)的安全分析66

4.4.1函數(shù)返回值的操作語義66

4.4.2非理想軌跡與理想軌跡67

4.5針對Needham-Schroeder協(xié)議與Diffie-Hellman協(xié)議及它們的改進協(xié)議在理想與攻擊

環(huán)境下的實驗68

4.5.1新方法實現(xiàn)的步驟68

4.5.2Needham-Schroeder協(xié)議及其改進協(xié)議實現(xiàn)的實驗69

4.5.3Diffie-Hellman協(xié)議及其改進協(xié)議實現(xiàn)的實驗77

4.5.4密碼協(xié)議實現(xiàn)的實驗分析84

4.6本章小結(jié)88

參考文獻88

第5章快速判斷密碼協(xié)議在代碼級上實現(xiàn)時導(dǎo)致的不安全原因

5.1相關(guān)研究工作92

5.2知識準(zhǔn)備92

目錄iii

5.2.1標(biāo)號遷移系統(tǒng)92

5.2.2密碼協(xié)議實現(xiàn)操作語義93

5.2.3密碼協(xié)議實現(xiàn)規(guī)范94

5.3新模型的建立94

5.3.1函數(shù)返回值字典94

5.3.2函數(shù)返回值序列95

5.3.3密碼協(xié)議代碼實現(xiàn)安全分析95

5.4針對經(jīng)典密碼協(xié)議的實驗與分析96

5.4.1NSL協(xié)議代碼實現(xiàn)的符號化規(guī)范97

5.4.2NSL協(xié)議部分源代碼標(biāo)注97

5.4.3NSL協(xié)議代碼實現(xiàn)的安全分析101

5.4.4新模型與原來模型比較103

5.5本章小結(jié)104

參考文獻105

第6章針對代碼底層匯編語言實現(xiàn)跳轉(zhuǎn)設(shè)計新的密鑰協(xié)商協(xié)議

6.1知識準(zhǔn)備109

6.1.1程序運行時寄存器的分配情況109

6.1.2程序調(diào)用（CALL）與返回（RET）操作情況110

6.1.3內(nèi)存溢出造成漏洞攻擊情況111

6.2改進的密鑰協(xié)商協(xié)議112

6.2.1基礎(chǔ)知識112

6.2.2改進的密鑰協(xié)商協(xié)議設(shè)計113

6.3改進的密鑰協(xié)商協(xié)議安全分析114

6.3.1基于密碼理論的安全分析114

6.3.2基于串空間的改進的密鑰協(xié)商協(xié)議實現(xiàn)的安全分析115

6.4基于RET改進的密鑰協(xié)商協(xié)議實驗116

6.4.1修改RET配件鏈117

6.4.2密鑰協(xié)商協(xié)議實驗118

6.4.3實驗結(jié)果與性能分析122

6.5本章小結(jié)124

參考文獻124

第7章基于內(nèi)容安全的密碼協(xié)議代碼實現(xiàn)行為安全

7.1相關(guān)研究工作128

7.2基礎(chǔ)知識129

7.2.1霍恩子句邏輯129

7.2.2密碼協(xié)議規(guī)范129

7.3新模型的建立與分析131

iv密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

7.3.1密碼協(xié)議的操作語義131

7.3.2建立密碼協(xié)議行為安全的分析模型132

7.4基于經(jīng)典密碼協(xié)議的新分析方法實驗133

7.4.1具體的實現(xiàn)步驟133

7.4.2模擬實驗134

7.5安全與性能分析135

7.5.1NSL協(xié)議描述135

7.5.2NSL協(xié)議代碼實現(xiàn)的安全分析137

7.5.3行為安全分析137

7.5.4新模型與現(xiàn)有分析模型比較138

7.6本章小結(jié)139

參考文獻139

第8章密碼協(xié)議的軟件實現(xiàn)安全分析

8.1軟件實現(xiàn)的物理層安全142

8.1.1側(cè)信道攻擊142

8.1.2密碼協(xié)議軟件實現(xiàn)的物理層安全147

8.2密碼防護方案的實現(xiàn)安全152

8.2.1掩碼方案安全性153

8.2.2軟件實現(xiàn)安全性分析155

8.2.3針對實際環(huán)境中軟件實現(xiàn)的安全性分析實驗161

8.2.4防護策略167

8.3本章小結(jié)169

參考文獻169

第9章總結(jié)與未來展望

9.1總結(jié)176

9.2未來展望178

參考文獻181

第1章緒論

在開放網(wǎng)絡(luò)空間中，密碼協(xié)議是保護信息安全傳輸[1]，嚴(yán)防信息在傳輸過程中隱私泄

露的關(guān)鍵技術(shù)[2]。迄今為止，設(shè)計一個安全、適用的密碼協(xié)議仍是研究者們關(guān)注的重點問

題之一。很多協(xié)議從設(shè)計到使用總會出現(xiàn)“使用→發(fā)現(xiàn)漏洞→修改→使用→發(fā)現(xiàn)漏洞

→……→修改→使用”的循環(huán)現(xiàn)象。這一現(xiàn)象說明密碼協(xié)議設(shè)計與安全實用之間仍存在

一定差距。因此，研究者們思考：能否在密碼協(xié)議設(shè)計階段就考慮它實現(xiàn)時的安全性？

為了解決這一問題，在密碼協(xié)議設(shè)計時，研究者們引入許多密碼協(xié)議分析方法（例如，

形式化、計算模型、計算可靠的形式化等），以便發(fā)現(xiàn)協(xié)議的漏洞，彌補協(xié)議實現(xiàn)時安全

性的不足。常用的密碼協(xié)議安全分析方法只能從理論上驗證或證明密碼協(xié)議的安全，無

法確保密碼協(xié)議實現(xiàn)的安全。只有當(dāng)密碼協(xié)議在轉(zhuǎn)換成軟件（程序源代碼）實現(xiàn)時被驗

證或證明是安全的，才能保證密碼協(xié)議是安全的。因此，密碼協(xié)議實現(xiàn)的安全分析與設(shè)

計是值得關(guān)注的方向，也是網(wǎng)絡(luò)空間安全領(lǐng)域研究的熱點之一。

1.1引言

一直以來，密碼協(xié)議安全驗證分析是衡量協(xié)議是否安全可靠的重要手段之一。隨著

大數(shù)據(jù)、云計算、物聯(lián)網(wǎng)和5G等技術(shù)的不斷成熟，傳統(tǒng)單一的端到端網(wǎng)絡(luò)通信模式已轉(zhuǎn)

換為多對一、多對多的新型網(wǎng)絡(luò)通信模式。在新型網(wǎng)絡(luò)環(huán)境下，通信信息更易受到攻擊，

用戶的隱私更易泄露[3,4]。因此，常用密碼協(xié)議的安全驗證分析方法已無法滿足新型網(wǎng)絡(luò)

通信模式下的信息安全需求，對密碼協(xié)議的安全分析與設(shè)計提出了更高要求[5]。

常用的密碼協(xié)議安全驗證分析只能驗證或證明協(xié)議的理論安全，無法確保密碼協(xié)議

在代碼級上實現(xiàn)時的安全。究其原因是沒有考慮下述幾種情況：

①程序設(shè)計語言的語法和語義結(jié)構(gòu)（例如，C語言內(nèi)存泄漏、指針越界、緩沖區(qū)溢

出等）；

②程序代碼執(zhí)行時產(chǎn)生很多臨時的異常情況（例如，函數(shù)調(diào)用的不確定返回值、程

序中斷、程序斷言等）；

③程序代碼實際執(zhí)行的運行環(huán)境（例如，不同網(wǎng)絡(luò)環(huán)境、不同語言環(huán)境等）。由此可

見，密碼協(xié)議實現(xiàn)時的安全驗證分析比形式化模型或計算模型下的密碼協(xié)議安全驗證分

析復(fù)雜。密碼協(xié)議實現(xiàn)的安全驗證，特別是在代碼級上實現(xiàn)時的安全分析與設(shè)計是網(wǎng)絡(luò)

空間安全領(lǐng)域研究的新方向[6]。

密碼協(xié)議實現(xiàn)的安全分析與設(shè)計作為網(wǎng)絡(luò)空間安全領(lǐng)域一個新的研究方向，在國內(nèi)

2密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

外處于起步階段。在國外，代碼級的密碼協(xié)議安全驗證分析的研究包括代碼模型提取[7]、

代碼自動生成[8]、操作語義分析[9]和精化（refinement）驗證分析[10]。在國內(nèi)，仍以常用

的安全驗證分析方法為主，例如，基于網(wǎng)關(guān)口令的認(rèn)證[11]、基于關(guān)鍵字域可變協(xié)議的驗

證[12]等。這些安全驗證分析基于計算語義安全來分析密碼協(xié)議的安全性，或用現(xiàn)有工具

和軟件檢測模型技術(shù)來驗證密碼協(xié)議是否安全[13,14]。而針對密碼協(xié)議實現(xiàn)時的安全分析

與設(shè)計相關(guān)研究少之又少。

密碼協(xié)議安全驗證分析是驗證或證明協(xié)議安全屬性是否成立，確保密碼協(xié)議在設(shè)計

上沒有缺陷，在代碼級上執(zhí)行時能避免漏洞產(chǎn)生。傳統(tǒng)的密碼協(xié)議安全驗證分析方法有

三類：形式化分析、計算模型分析和計算可靠的形式化分析。

（1）密碼協(xié)議形式化分析

形式化分析是對協(xié)議的各要素進行抽象符號化，然后基于邏輯的推導(dǎo)，從而發(fā)現(xiàn)密

碼協(xié)議中的缺陷。文獻[15]正式提出密碼協(xié)議安全驗證的形式化分析，形成以Dolev-Yao

模型假設(shè)[16]為基礎(chǔ)的形式化安全分析方法。文獻[17]首次在密碼協(xié)議的形式化分析中應(yīng)用

BAN邏輯推導(dǎo)，基于BAN邏輯的形式化安全驗證分析方法是密碼協(xié)議安全分析的一個里

程碑。

（2）密碼協(xié)議計算模型分析

計算模型分析采用概率大小衡量密碼協(xié)議的安全性，其理論基礎(chǔ)為計算理論（例如，

可忽略函數(shù)、多項式時間和計算不可區(qū)分性等），并涉及困難數(shù)學(xué)問題（例如，大整數(shù)因

式分解、離散對數(shù)和橢圓曲線等）。相關(guān)研究可見文獻[18][19][20]。

（3）密碼協(xié)議計算可靠的形式化分析

計算可靠的形式化分析是形式化模型與計算模型有機結(jié)合的一種密碼協(xié)議安全驗證

分析方法。該分析方法是指如果密碼協(xié)議在形式化模型下安全，則在計算模型下也必然

安全，即密碼協(xié)議安全屬性的形式化分析與計算模型分析是等價的，該分析方法的代表

模型是AbadiRogway模型[21]（簡稱AR模型）?；贏R分析方法，文獻[22]進一步提出

密碼協(xié)議計算語義與形式化模型結(jié)合的分析方法，基于邏輯語義分析方法來分析密碼協(xié)

議的安全性。文獻[23]證明協(xié)議屬性在計算語義與形式化兩種不同的模型下都是安全的，

即密碼協(xié)議安全屬性的可靠性（soundness:表示在交互式證明系統(tǒng)中兩個狀態(tài)或模型變換

時，某一屬性變化的概率可忽略不計，即協(xié)議屬性可靠）是等價的。文獻[24]提出自動的

密碼協(xié)議安全可靠性證明，提升了密碼協(xié)議安全屬性的可靠性，并在實際中得到應(yīng)用[25]。

基于計算語義與形式化模型，文獻[14]提出剛性與相似性概念的安全驗證分析方法。這種

分析方法以密碼協(xié)議語法和語義賦值為理論，從而構(gòu)建有攻擊能力模型的非自由消息代

數(shù)理論框架，同時證明協(xié)議在該框架內(nèi)滿足安全的可靠性。

常用的密碼協(xié)議安全驗證分析已取得豐碩的成果[6]，但并沒有考慮密碼協(xié)議代碼級上

實際執(zhí)行時存在的問題：

第1章緒論3

①程序語言結(jié)構(gòu)困難（例如，C語言的內(nèi)存泄漏、Java封裝、F#語義等）；

②從密碼協(xié)議規(guī)范到代碼執(zhí)行產(chǎn)生漏洞（例如，程序中斷、變量的不正確使用等）；

③程序代碼執(zhí)行跡的困難（例如，代碼的消息匹配、函數(shù)調(diào)用的不正確返回值等）；

④程序代碼執(zhí)行的行為困難（例如，在具體狀態(tài)空間下，密碼協(xié)議的屬性驗證）。要

解決這一系列問題，需拓展密碼協(xié)議在代碼級上實現(xiàn)時的安全分析與設(shè)計方法。

1.2關(guān)鍵技術(shù)

代碼級上實現(xiàn)的安全驗證分析有助于發(fā)現(xiàn)協(xié)議設(shè)計階段不容易發(fā)現(xiàn)的問題（例如，

緩沖區(qū)溢出和密碼協(xié)議設(shè)計的缺陷），這些問題往往在密碼協(xié)議實現(xiàn)過程中才被發(fā)現(xiàn)，把

密碼協(xié)議在代碼級實現(xiàn)的安全因素作為設(shè)計前提，可以有效避免漏洞的產(chǎn)生以及利用漏

洞進行的攻擊。如果把密碼協(xié)議代碼實現(xiàn)時的安全性引入到設(shè)計階段，可以有效地預(yù)防

和避免協(xié)議代碼實現(xiàn)過程中漏洞的產(chǎn)生和遭受利用漏洞的攻擊（例如，代碼重用攻擊和

shellcode注入攻擊），從而達到密碼協(xié)議設(shè)計的目的。

1．非簽名認(rèn)證的密鑰協(xié)商協(xié)議設(shè)計研究方法

密鑰協(xié)商協(xié)議廣泛應(yīng)用于各種網(wǎng)絡(luò)環(huán)境中，例如，無線傳感器網(wǎng)絡(luò)、IoT（Internetof

Things，物聯(lián)網(wǎng)）網(wǎng)絡(luò)和云計算環(huán)境等。目前，現(xiàn)有的密鑰協(xié)商協(xié)議為保證交互式通信中

的安全，常常引入額外的安全技術(shù)（簽名和認(rèn)證等）。額外的簽名認(rèn)證技術(shù)增加了密鑰協(xié)

商協(xié)議實現(xiàn)時的計算量，不適用于計算能力有限的移動終端通信設(shè)備的通信。如何設(shè)計

出計算量少且又安全的密鑰協(xié)商協(xié)議是研究者們思考的問題。針對這種情況，基于二叉

樹特點，設(shè)計一種新的密鑰協(xié)商協(xié)議[29]，該密鑰協(xié)商協(xié)議具有計算量少、使用強安全假

設(shè)少的優(yōu)點。

2．通過密碼協(xié)議在代碼級上實現(xiàn)時的軌跡行為是否異常的研究方法

根據(jù)自動機原理，程序運行實質(zhì)上是狀態(tài)之間的轉(zhuǎn)換，這種轉(zhuǎn)換表現(xiàn)出程序代碼實

現(xiàn)的行為。只有當(dāng)密碼協(xié)議轉(zhuǎn)換成某一種具體程序語言代碼時才能體現(xiàn)其價值。程序語

言在代碼實現(xiàn)時函數(shù)之間的調(diào)用是必不可少的，例如，C/C++語言、Java語言和Python

語言等。函數(shù)調(diào)用得到的函數(shù)返回值影響程序流的走向，從而影響密碼協(xié)議交互式通信

的行為?；谶@一觀點，根據(jù)程序代碼實現(xiàn)時函數(shù)返回值軌跡的變化來分析密碼協(xié)議實

現(xiàn)的安全性[26]。

3．快速判斷密碼協(xié)議在代碼級上實現(xiàn)時導(dǎo)致不安全原因的研究方法

密碼分析模型一直以來都是信息安全研究的重點之一，特別是分析密碼協(xié)議代碼實

現(xiàn)的安全模型值得關(guān)注。針對密碼協(xié)議代碼實現(xiàn)的安全分析，本書提出一種基于字典序

列模型的密碼協(xié)議代碼實現(xiàn)的安全分析方法[27]。這種方法是在密碼協(xié)議代碼實現(xiàn)時，通

過函數(shù)返回值序列的變化來分析協(xié)議實現(xiàn)是否安全?；谛履Ｐ偷陌踩治龇椒ǎo出

經(jīng)典密碼協(xié)議實現(xiàn)的實例。實驗結(jié)果表明，新模型方法相比以前的模型分析方法更好。

4密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

新模型方法的提出為密碼協(xié)議實現(xiàn)的設(shè)計、評估和測試提供了幫助。

4．針對代碼底層匯編語言實現(xiàn)跳轉(zhuǎn)設(shè)計新的密鑰協(xié)商協(xié)議的研究方法

目前，大多數(shù)密鑰協(xié)商協(xié)議還是基于Dolev-Yao模型假設(shè)來評估其安全性，在密鑰協(xié)

商協(xié)議設(shè)計階段未考慮代碼實現(xiàn)時的安全性。這導(dǎo)致密鑰協(xié)商協(xié)議代碼實現(xiàn)時會出現(xiàn)很

多不安全的問題（例如，緩沖區(qū)溢出、注入攻擊和代碼重用攻擊等）?；诔绦虼a實現(xiàn)

時的函數(shù)返回的RET指令值，設(shè)計一種新的密鑰協(xié)商協(xié)議[28]。該方案在密鑰協(xié)商協(xié)議設(shè)

計階段就考慮其代碼實現(xiàn)時的安全性。該方案不僅考慮協(xié)議理論上的安全，而且考慮協(xié)

議實現(xiàn)時防止代碼重用攻擊和緩沖區(qū)溢出攻擊等問題。

5．基于內(nèi)容安全的密碼協(xié)議代碼實現(xiàn)行為安全的研究方法

安全分析模型是密碼安全實現(xiàn)的重要保障，行為安全是信息安全研究的內(nèi)容之一。

現(xiàn)有的分析模型僅僅從理論上保證密碼協(xié)議實現(xiàn)的安全，而沒有考慮密碼協(xié)議實現(xiàn)時的

行為安全（例如，無線網(wǎng)絡(luò)中的拒絕服務(wù)、會話劫持和程序漏洞攻擊等）。密碼協(xié)議實現(xiàn)

的行為是否安全，取決于其實現(xiàn)時的行為是否異常，所以針對密碼協(xié)議實現(xiàn)的行為安全

模型被提出[30]。該模型將密碼協(xié)議實現(xiàn)的行為定義為外部行為和內(nèi)部行為兩個部分。外

部行為是指開放網(wǎng)絡(luò)空間實體之間交互通信的行為；內(nèi)部行為是指密碼協(xié)議編碼程序源

代碼實現(xiàn)的行為。通過外部行為與內(nèi)部行為的異常分析，從而發(fā)現(xiàn)、控制或糾正密碼協(xié)

議實現(xiàn)的異常行為，掌握對密碼協(xié)議實現(xiàn)行為的可控性。為驗證該模型的可控性，本章

以經(jīng)典協(xié)議密碼協(xié)議為實例進行模擬實驗，并驗證了密碼協(xié)議實現(xiàn)是安全可控的。

6．密碼協(xié)議軟件實現(xiàn)的物理層安全分析的研究方法

隨著掩碼的發(fā)展，對應(yīng)的攻擊技術(shù)也不斷提升，針對一階或高階掩碼防護方案，對

應(yīng)出現(xiàn)了二階功耗分析[31]和高階功耗分析[32]，其攻擊原理與一階功耗分析相似，在進行

區(qū)分器分析之前需要對不同掩碼操作對應(yīng)的功耗點利用組合函數(shù)進行預(yù)處理。攻擊方法

不斷追求著優(yōu)化泄露模型與區(qū)分器模型，尋求更低復(fù)雜度或其他角度去攻擊。

基于密碼協(xié)議實現(xiàn)的安全性考慮，針對密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計，本書

分別從密碼協(xié)議設(shè)計、密碼協(xié)議源代碼實現(xiàn)的行為安全、基于匯編語言的密碼協(xié)議源代

碼底層實現(xiàn)的安全和密碼協(xié)議實現(xiàn)的側(cè)信道攻擊等方面的研究進行探討。

1.3本書結(jié)構(gòu)介紹

本書內(nèi)容共分為9章，下面來簡要了解一下各章的主要內(nèi)容。

第1章緒論。本章介紹研究的背景與意義，陳述國內(nèi)外研究現(xiàn)狀以及研究內(nèi)容，最

后給出本書的組織結(jié)構(gòu)。

第2章密碼協(xié)議實現(xiàn)安全的研究現(xiàn)狀。本章分別介紹代碼模型提取安全驗證、代碼

自動生成安全驗證、基于操作語義安全驗證、密碼協(xié)議精化安全驗證等研究內(nèi)容。

第3章非簽名認(rèn)證的密鑰協(xié)商協(xié)議設(shè)計。為了滿足計算能力有限的通信設(shè)備，基于

第1章緒論5

二叉樹特點和同態(tài)映射設(shè)計了一種非簽名認(rèn)證的新密鑰協(xié)商協(xié)議。該密鑰協(xié)商協(xié)議沒有

使用額外的簽名認(rèn)證技術(shù)，所以在協(xié)商共享密鑰時，具有計算量少和強安全假設(shè)少等優(yōu)

點，適用于計算能力有限的移動通信設(shè)備。

第4章通過密碼協(xié)議在代碼級上實現(xiàn)時的軌跡行為是否異常來評估其安全性?；?/p>

程序代碼實現(xiàn)時的函數(shù)返回的RET指令值，設(shè)計一種新的密鑰協(xié)商協(xié)議。該方案在密鑰

協(xié)商協(xié)議設(shè)計階段就考慮其代碼實現(xiàn)時的安全性。該方案不僅考慮協(xié)議理論上的安全，

而且考慮協(xié)議實現(xiàn)時防止代碼重用攻擊和緩沖區(qū)溢出攻擊等問題。

第5章快速判斷密碼協(xié)議在代碼級上實現(xiàn)時導(dǎo)致的不安全原因。使用密碼協(xié)議代碼

實現(xiàn)的函數(shù)返回值組成的跡，分析協(xié)議實現(xiàn)的安全。具體以經(jīng)典的密碼協(xié)議

（Needham-Schroeder協(xié)議和Diffie-Hellman協(xié)議）為實例，分析密碼協(xié)議代碼實現(xiàn)時的

中間人攻擊情況。通過理論分析與實驗表明該方法是可行和有效的。

第6章針對代碼底層匯編語言實現(xiàn)跳轉(zhuǎn)設(shè)計新的密鑰協(xié)商協(xié)議。攻擊者利用程序漏

洞改變RET值，導(dǎo)致程序?qū)崿F(xiàn)順序被攻擊者任意控制，嚴(yán)重地影響密碼協(xié)議實現(xiàn)的安全

性。設(shè)計一種基于RET配件鏈的新密鑰協(xié)商協(xié)議。該密鑰協(xié)商協(xié)議不僅考慮密碼技術(shù)上

的安全，而且考慮程序代碼實現(xiàn)時的控制流完整性，防止密鑰協(xié)商協(xié)議實現(xiàn)時程序漏洞

的攻擊和代碼重用攻擊。

第7章基于內(nèi)容安全的密碼協(xié)議代碼實現(xiàn)行為安全。設(shè)計一種基于密碼協(xié)議實現(xiàn)的

行為安全分析模型。該模型把密碼協(xié)議實現(xiàn)分為兩部分：一是外部行為（開放網(wǎng)絡(luò)空間

交互通信的行為）；二是內(nèi)部行為（代碼實現(xiàn)的行為）。通過行為的可控性，能夠發(fā)現(xiàn)、

控制或糾正密碼協(xié)議實現(xiàn)的安全?；谠摲治瞿Ｐ头椒ǎ菊乱越?jīng)典的密碼協(xié)議為實例

進行模擬實驗。實驗結(jié)果表明，密碼協(xié)議實現(xiàn)的行為安全是可控的。

第8章密碼協(xié)議的軟件實現(xiàn)安全分析。本章介紹針對密碼協(xié)議編碼成為軟件實現(xiàn)的

物理層安全，以密碼協(xié)議實現(xiàn)的側(cè)信道攻擊為主，探討一階或高階掩碼防護方案，闡述

密碼軟件實現(xiàn)的安全性。

第9章總結(jié)與未來展望。本章介紹對研究內(nèi)容進行了總結(jié)，并對未來的工作進行

展望。

參考文獻

[1]張煥國,韓文報,來學(xué)嘉,等.網(wǎng)絡(luò)空間安全綜述[J].中國科學(xué):信息科學(xué)，2016,46(2):125-164.

[2]章睿,薛銳,林東岱.海云安全體系架構(gòu)[J].中國科學(xué):信息科學(xué)，2015,45(6):796-816.

[3]馮登國,張敏,李昊.大數(shù)據(jù)安全與隱私保護[J].計算機學(xué)報，2014,37(1):246-258.

[4]陳克非,翁健.云計算環(huán)境下數(shù)據(jù)安全與隱私保護[J].杭州師范大學(xué)學(xué)報（自然科學(xué)版），

2014,13(6):561-571.

[5]曹珍富.密碼學(xué)的新發(fā)展[J].四川大學(xué)學(xué)報（工程科學(xué)版），2015,47(1):1-12.

6密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

[6]雷新鋒,宋書民,劉偉兵,等.計算可靠的密碼協(xié)議形式化分析綜述[J].計算機學(xué)報，2014，37(5)：

993-1016.

[7]BHARGAVANK,FOURNETC,ANDREWDG,eta1.Verifiedinteroperableimplementations

ofsecurityprotocols[J].ACMTransactionsonProgrammingLanguagesandSystems,2008,31(1):1-61.

[8]O’SHEAN.VerificationandValidationofSecurityProtocolImplementations[D].Schoolof

Informatics,UniversityofEdinburgh,UK,2010.

[9]CREMERSC,MAUWS.OperationalSemanticsandVerificationofSecurityProtocols[J].

Springer-VerlagBerlinHeidelberg,2012.

[10]ABADIM,LAMPORTL.Theexistenceofrefinementmapping[J].TheoreticalComputer

Science,1992,82:253-284.

[11]魏福山，張振峰，馬傳貴.標(biāo)準(zhǔn)模型下網(wǎng)關(guān)口令認(rèn)證密鑰交換協(xié)議的通用框架[J].計算機學(xué)

報,2012,35(9)：1833-1843.

[12]苗銀賓，馬建峰，劉志全，等.關(guān)鍵字域可變的可驗證密文檢索[J].西安電子科技大學(xué)學(xué)報

（自然科學(xué)版）,2017,44(1)：57-63.

[13]唐朝京,魯智勇,馮超.基于計算語義的安全協(xié)議驗證邏輯[J].電子學(xué)報,2014,6(42):1179-1185.

[14]田園,王穎,金鋒,等.基于剛性與相似性概念的密碼協(xié)議分析方法[J].計算機學(xué)報，

2009,32(4):618-634.

[15]NEDDHAMRM,SCHROEDERMD.Usingencryptionforauthenticationinlargenetworksof

computers[J].CommuicaonsoftheACM,1978,21(12):993-999.

[16]DOLEVD,YAOAC.Onthesecurityofpublickeyprotocols[C]//Proceedingsofthe22nd

SymposiumonFoundationofComputerScience.Oakland,USA.1981:350-357.

[17]BURROWSM,ABADIM,NEEDHAMR.Alogicofauthentication[R].PaloAlto,USA:Digital

EquipmentCorp,SystemsResearchCenter,1989:39.

[18]BLUM,MICALIS.Howtogeneratecryptographicallystrongsequencesofpseudorandom

bits[C]//Proceedingsofthe23rdAnnualSymposiumonFoundationsofComputerScience.Los

Alamitos,USA,1982:112-117.

[19]YAOAC.Theoryandapplicationoftrapdoorfunctions[C]//proceedingsofthe23rdIEEE

SymposiumonFoundationsofComputerScience.Califonia,USA,1982:80-91.

[20]GOLDWASSERS,MICALIS.Probabilisticencryption[J].JournalofCompterandSystemSciences,

1984,28(2):270-299.

[21]ABADIM,ROGAWAYP.Reconcilingtwoviewsofcryptography:thecomputational

soundnessofformalencryption[J].JournalofCryptology,2002,15(2):103-127.

[22]MICCIANCIOD,WARINSCHIB.CompletenesstheoremsfortheAbadi-Rogawaylogicof

encryptedexpressions[J].JournalofComputerSecurity,2004,12(1):99-129.

第1章緒論7

[23]BLANCHETB.Computationallysoundmechanizedproofsofcorrespondenceassertions[C]//

Proceedingsofthe20thIEEEComputerSecurityFoundationsSymposium.Venice,Italy,2007:97-111.

[24]CORTIERV,WARINSHIB.Computationallysound,automatedproofsforsecurityprotocol

analysis[J].LogicalMethodsinComputerScience,2007,3(3),396-458.

[25]BACKESM,PFITZMANB,WAIDNERA.Acomposablecryptographiclibrarywithnested

operations[C]//Proceedingsofthe10thACMConferenceofComputerandCommunicationsSecurity,

NewYork,UK,2003:122-136.

[26]WUFS,ZHANGHG,WANGWQ,etal.ANewMethodtoAnalyzetheSecurityofProtocol

ImplementationsBasedonIdealTrace[J].SecurityandCommunicationNetworks,Volume2017:1-15.

[27]WUFS,ZHANGHG.ADictionarySequenceModeltoAnalyzetheSecurityofProtocol

ImplementationsattheSourceCodeLevel[J].ChineseConferenceonTrustedComputingand

InformationSecurity.23November2017:126-142.

[28]WUFS，ZHANGHG，NIMT，etal.ANovelKeyAgreementProtocolBasedonRETGadgetChains

forPreventingReusedCodeAttacks[J].IEEEAccess.2018，6:70820-70830.

[29]吳福生,張煥國.基于二叉樹的非簽名認(rèn)證密鑰協(xié)商協(xié)議[J].計算機研究與發(fā)展.

2017,54(12):2797-2804.

[30]吳福生,張煥國,倪明濤,等.基于密碼協(xié)議實現(xiàn)的行為安全分析模型[J].山東大學(xué)學(xué)報（理學(xué)

版）.2019,54(3):1-11.

[31]OSWALDE,MANGARDS,HERBSTC,etal.Practicalsecond-orderDPAattacksformasked

smartcardimplementationsofblockciphers[C].Cryptographers’TrackattheRSAConference.Springer,

Berlin,Heidelberg,2006:192-207.

[32]LEMKERUSTK,PAARC.GaussianMixtureModelsforHigher-OrderSideChannelAnalysis[M].

CryptographicHardwareandEmbeddedSystems-CHES2007.SpringerBerlinHeidelberg,2007:14-27.

第2章密碼協(xié)議實現(xiàn)安全的研究現(xiàn)狀

從應(yīng)用的角度看，密碼協(xié)議最終以程序代碼形式表現(xiàn)，其作用需落到代碼實現(xiàn)上去。

因此，一個密碼協(xié)議是否安全適用，最終還得看協(xié)議的代碼實現(xiàn)是否安全適用。由于密

碼協(xié)議代碼實現(xiàn)環(huán)境復(fù)雜，在分析它的安全性時會產(chǎn)生這樣的問題：即使經(jīng)過理論證明

安全的協(xié)議，在其代碼實現(xiàn)過程中，若引入新的不安全因素，則會導(dǎo)致密碼協(xié)議代碼實

現(xiàn)時的不安全。究其原因是沒有考慮下述幾種情況：

①程序語言的語法和語義結(jié)構(gòu)不完善（例如，C語言指針越界和緩沖區(qū)溢出等）；

②程序代碼實現(xiàn)時會產(chǎn)生臨時的異常情況（例如，函數(shù)調(diào)用返回值的不確定性、程

序中斷和程序斷言）；

③程序代碼實現(xiàn)在不同的運行環(huán)境（例如，網(wǎng)絡(luò)環(huán)境與語言環(huán)境等）下實現(xiàn)。

由此可見，密碼協(xié)議代碼實現(xiàn)的安全分析方法比常用的安全分析方法復(fù)雜。密碼協(xié)

議代碼實現(xiàn)的安全分析是保證信息安全傳輸?shù)年P(guān)鍵技術(shù)?，F(xiàn)已發(fā)展成為信息安全研究的

新方向[1]。漏洞對軟件的危害是工業(yè)界與學(xué)術(shù)界關(guān)注的信息安全重點問題之一。漏洞產(chǎn)生

原因：

一是軟件設(shè)計不完善，存在缺陷；

二是程序設(shè)計語言自身有缺陷。

最值得關(guān)注的是C與C++等計算機程序語言中普遍存在漏洞。例如，計算機指令

可對內(nèi)存直接存??；C與C++語言對用戶的輸入沒有自動的邊界檢查機制，以及對釋放

的指針再次利用[2]。導(dǎo)致利用基于緩沖區(qū)溢出[3]漏洞的代碼重用攻擊。代碼重用攻擊是利

用程序漏洞的一種典型攻擊行為，而且具有遠(yuǎn)程特征，破壞性極大。攻擊者可以靈活使

用代碼重用攻擊繞過當(dāng)前很多防御機制。因此，這種攻擊在國際學(xué)術(shù)界引起了極大的關(guān)

注。例如，2017年WannaCry勒索病毒，本質(zhì)上是攻擊者利用WindowsSMB協(xié)議的漏

洞，通過遠(yuǎn)程實施代碼來提升自身系統(tǒng)權(quán)限而實施的一種攻擊。2015—2020年間在國際

頂級的安全會議[CCS（ACMConferenceonComputerandCommunicationsSecurity）、S&P

（IEEESymposiumonSecurityandPrivacy）和USENIX(USENIXSecuritySymposium)和

NDSS（NetworkandDistributedSystemSecuritySymposium）]發(fā)表大量有密碼協(xié)議安全分

析的學(xué)術(shù)論文。

密碼協(xié)議屬于軟件的范疇，同樣可能遭受因程序語言結(jié)構(gòu)缺陷所帶來的攻擊。例如，

2014年4月8日，研究人員發(fā)現(xiàn)OpenSSL的源代碼中存在一個漏洞，可以讓攻擊者

獲得服務(wù)器上64K內(nèi)存中的數(shù)據(jù)內(nèi)容，并為其起了個形象的名字：心臟出血[4]。導(dǎo)致這

第2章密碼協(xié)議實現(xiàn)安全的研究現(xiàn)狀9

次事件的直接原因是OpenSSL協(xié)議源代碼中的C語言部分函數(shù)無法完成邊界檢測。

TLS協(xié)議是廣泛使用的應(yīng)用協(xié)議。針對密碼協(xié)議的安全性研究出現(xiàn)了很多研究成果（最

近五年，在四大國際頂級系統(tǒng)安全會議發(fā)表關(guān)于密碼協(xié)議的研究成果，如表2-1所示）。

由此可見，基于密碼協(xié)議安全分析與設(shè)計越來越受到學(xué)術(shù)界與工業(yè)界的重視。

表2-1發(fā)表與密碼協(xié)議相關(guān)論文統(tǒng)計表

年份201520162017201820192020

篇數(shù)111317161915

密碼協(xié)議代碼實現(xiàn)的安全分析與設(shè)計不同于傳統(tǒng)的方法，不管是協(xié)議的安全分析還

是設(shè)計新的協(xié)議，都是基于協(xié)議代碼實現(xiàn)時的安全性來考慮，這也正是研究者們希望達

到的目標(biāo)。如果設(shè)計新的協(xié)議時不考慮它的代碼實現(xiàn)情況，就不能從代碼實現(xiàn)上去分析

其安全性，這樣往往導(dǎo)致協(xié)議代碼實現(xiàn)時發(fā)生錯誤。密碼協(xié)議代碼實現(xiàn)的安全分析是信

息安全的關(guān)鍵環(huán)節(jié)，是協(xié)議實現(xiàn)安全的重要保障，在整個通信安全中起到關(guān)鍵作用。

2.1代碼模型提取安全驗證分析

模型提取方法來源于程序?qū)傩缘某橄蠼忉屨揫5]和經(jīng)典的抽象理論[6]。代碼模型提取是

把密碼協(xié)議的某一具體屬性映射成它的某一抽象屬性，并證明如果抽象屬性成立，那么

具體屬性也成立。

MMP,E=()

不妨設(shè)P是協(xié)議，E是環(huán)境，M為建模，具體協(xié)議模型為c；α()?是抽象映

α()M?

射，則抽象模型為c。不妨設(shè)為密碼協(xié)議的具體屬性，它對應(yīng)的抽象屬性為α()?。代

α()Mα()?→M?→

碼模型提取的數(shù)學(xué)表示為c├c├，其中，“├”表示推導(dǎo)，“”表示蘊含。

由此可見，代碼模型提取考慮兩個因素：

①映射函數(shù)α()?的可靠性。文獻[7]把密碼協(xié)議代碼（用C語言編寫程序代碼）的注

釋假設(shè)為可信任項，并把它作為模型提取研究的一部分；

②協(xié)議環(huán)境（例如，語言特征，程序運行的環(huán)境等）。由于Java語言、F#語言等是具

有良好封裝性的高級語言，所以在代碼模型提取中側(cè)重于考慮程序運行的環(huán)境問題。

不同程序設(shè)計語言的語義、語法、句法不盡相同。例如，C語言考慮指針，Java語

言進行封裝，F(xiàn)#語言具有相對完備的語義且封裝程度更高。下面分別介紹基于C、Java、

F#三種語言的密碼協(xié)議代碼模型來提取安全驗證分析。

2.1.1C語言模型提取分析

C語言的主要特點是指針運算和函數(shù)，但密碼協(xié)議的規(guī)范無法表達C語言的內(nèi)部函

數(shù)（例如，allocation,pointer等）與外部函數(shù)庫（例如，memcpy、strcpy等）的鏈接，這

使密碼協(xié)議代碼安全驗證分析變得復(fù)雜和困難。為解決這一矛盾，C語言代碼模型提取把

具體模型的協(xié)議代碼映射為抽象模型的協(xié)議規(guī)范，然后根據(jù)抽象模型的協(xié)議規(guī)范進行安

10密碼協(xié)議實現(xiàn)的邏輯安全分析與設(shè)計

全驗證分析。本小節(jié)從以下三個方面介紹C語言的密碼協(xié)議代碼模型提取。

（1）基于信任斷言分析

信任斷言分析是一種C語言代碼模型提取的協(xié)議代碼執(zhí)行安全驗證分析方法，由內(nèi)

部和外部兩個模型組成。它將密碼協(xié)議代碼安全驗證的復(fù)雜性與困難性作為信任假設(shè)，

構(gòu)建密碼協(xié)議代碼實際執(zhí)行時的內(nèi)部信任（InternalTrust）和外部信任（ExternalTrust）。

文獻[7]首次提出信任斷言模型的C語言代碼模型提取分析方法。該方法使用霍恩子句邏

輯（HornClausesLogic）來表示密碼協(xié)議規(guī)范和攻擊者的能力。它假設(shè)密碼協(xié)議代碼執(zhí)

行的C語言指針運算為內(nèi)部信任，建立信任斷言模型（TrustAssertionsModel）對協(xié)議進

行安全驗證分析。

①外部信任斷言模型（ExternalTrustAssertionsModel，ETAM）假設(shè)攻擊者擁有信任

斷言的能力（knows作為謂詞，knows（X）表示攻擊者具有獲得X知識的能力），如表2-2

所示。

②內(nèi)部信任斷言模型（InternalTrustAssertionsModel，ITAM）假設(shè)C語言內(nèi)部的編

譯序列為信任斷言。

表2-2外部信任斷言模型

霍恩子句模型化入侵者能力

knows(nil)

入侵者建立列表

knows(cons(X,Y))<-knows(X),knows(Y)

knows(X)<-knows(cons(X,Y))

入侵者讀取列表所有基本信息

knows(Y)<-knows(cons(X,Y))

knows(crypt(X,Y))<-knows(X),knows(Y)入侵者能夠加密

knows(pub(X))入侵者知道公鑰

knows(X)<-knows(crypt(X,pub(Y))),knows(prv(Y))

knows(X)<-knows(crypt(X,prv(Y))),

knows(pub(Y))入侵者用他知道的解密密鑰能夠解密密文

knows(X)<-knows(crypt(X,sk(Y,Z))),

knows(sk(Y,Z))

x,t∈AtomPQQQn←≠,,,,
0

設(shè)，xrect表示x信任t。根據(jù)霍恩子句邏輯表示（12n，

P表示過程名；Qi表示過程調(diào)用，且in∈）可知，邏輯表達式成立：

xtrec←xrect

11

（2-1）

xrectxt,,
rec

22nn

這里的xirecti表示xi信任ti。例如，一條簡單的C語言代碼：msg?>id_[]10=id[]0，根

據(jù)C語言內(nèi)部編譯可得到編譯序列如下：

第2章密碼協(xié)議實現(xiàn)安全的研究現(xiàn)狀11

zx==0&id,,[]zxx=?

121

x=→_1（）

3msgid2-2

xxzxx=?=[],

4342

由式（2-1）和式（2-2）得到表達式（2-3）成立：

zrec0,xrecid[]z

1

xxx?→,_（）

213recrecmsgid12-3

xxzxx[],?

43rec42rec

由霍恩子句邏輯可知式（2-4）成立：

msg?>id_[]10recid[]0←

zx,[]z

rec01recid

（2-4）

xxx?→,_1

213recrecmsgid

xxzxx[],?

43rec4rec2

由此可見，基于信任斷言的具體分析過程是密碼協(xié)議源代碼經(jīng)過C語言內(nèi)部編譯后，

得到一些有序的編譯序列，通過霍恩子句邏輯推導(dǎo)得到ITAM編譯序列。根據(jù)ITAM和

ETAM對密碼協(xié)議代碼執(zhí)行的安全驗證分析。

文獻[7]提出信任斷言方法考慮到密碼協(xié)議代碼實際執(zhí)行的情況，但無法解決密碼協(xié)

議代碼執(zhí)行的具體行為（例如，初始化加密、解密和Hash函數(shù)[8]等），也沒有考慮到C語

言數(shù)組越界[9]和緩沖區(qū)溢出[10]等情況，更沒有考慮到密碼協(xié)議的安全認(rèn)證。基于信任斷言

模型的密碼協(xié)議安全驗證分析仍有待進一步完善。有進一步需求的讀者，請參考文獻[7]

中的相關(guān)內(nèi)容。

（2）基于自動化分析

自動模型提取采用自動模型框架對密碼協(xié)議代碼執(zhí)行進行自動安全驗證分析。文獻

[11]提出基于C語言的ASPIER（AutomatedSecurityProtocolImplementationverifyER，

自動模型框架的密碼協(xié)議代碼）執(zhí)行安全驗證分析方法，該方法使用ASPIER自動模型框

架對OpenSSL進行安全驗證分析。文獻[12]提出VCC（VerifyingConcurrentC）并發(fā)框架

和多線程的安全驗證分析，適用于通用自動模型提取的密碼協(xié)議代碼執(zhí)行安全驗證分析。

①ASPIER自動分析。這種分析是基于軟件模型檢測標(biāo)準(zhǔn)的安全驗證分析方法。在具

體的密碼協(xié)議代碼執(zhí)行自動模型提取分析中，用狀態(tài)規(guī)范機制SSMs（SSMs=specification

statsmachines）取代C語言庫函數(shù)，對密碼協(xié)議安全屬性進行驗證分析。ASPIER有類似

于C語言的語法結(jié)構(gòu)。因此，ASPIER自動分析適用于代碼級的密碼協(xié)議安全驗證分析。

與C語言不同，ASPIER有自己的語言結(jié)構(gòu)和驗證方法，即把密碼協(xié)議的C語言源代碼

轉(zhuǎn)換為類似于C語言的抽象偽代碼。ASPIER自動分析表現(xiàn)在自動驗證、作為抽象工具和

12密碼協(xié)