近年來,網(wǎng)絡(luò)安全問題日趨嚴(yán)重,針對計算機網(wǎng)絡(luò)的安全和隱私研究已刻不容緩。為了解決網(wǎng)絡(luò)協(xié)議安全性不足的問題,研究人員設(shè)計了各種網(wǎng)絡(luò)安全協(xié)議（以下簡稱安全協(xié)議）,以增強網(wǎng)絡(luò)的安全。但是,很多投入實際應(yīng)用的安全協(xié)議在運行時并不能提供其聲明的安全服務(wù)。因此,針對安全協(xié)議的安全性檢測成為安全測試中的重要環(huán)節(jié)。研究人員在設(shè)計或優(yōu)化安全協(xié)議后,需要進(jìn)一步證明該協(xié)議的安全。與非形式化的安全協(xié)議驗證技術(shù)相比,形式化方法能夠更全面、深入的檢測安全協(xié)議和軟件中未知的漏洞,它不僅能夠證明安全協(xié)議的安全性,而且有助于發(fā)現(xiàn)針對安全協(xié)議的新型攻擊手段。但是由于安全協(xié)議的復(fù)雜性,現(xiàn)有的形式化驗證技術(shù)并不能自動化證明所有的安全協(xié)議,在證明過程中需要專業(yè)驗證人員輔助計算機完成證明。過高的人力成本和學(xué)習(xí)成本阻礙了形式化驗證技術(shù)的進(jìn)一步發(fā)展和運用。本文圍繞安全協(xié)議的形式化自動驗證相關(guān)問題,開展了深入的研究。主要研究成果總結(jié)如下:1.提出了一種基于強化學(xué)習(xí)的安全協(xié)議形式化自動驗證技術(shù),設(shè)計并實現(xiàn)了原型系統(tǒng)。本方法突破并解決了傳統(tǒng)形式化自動驗證中的狀態(tài)空間爆炸問題。相比于傳統(tǒng)的形式化驗證工具,該系統(tǒng)可以全自動地搜索正確證明路徑,... 

【文章來源】：中國科學(xué)技術(shù)大學(xué)安徽省211工程院校985工程院校

【文章頁數(shù)】：117 頁

【學(xué)位級別】：博士

【部分圖文】：

圖３．４安全協(xié)議通用全自動形式化驗證系統(tǒng)框架??

?１?——Ｉ???１０?＾００８８８???１？?Ｉｃ８６４ｇ４０?Ｒｕｌｅ?�。耍眨�?）?９?？ｖｋ?Ｒｕｌｅ?ＩＫＵ（－ｉｉ）?§）?？ｖｔ．ｌ??Ｓｔｅｐ?２?Ｓｔｅｐ?２??????．Ｒｕｌｅ?丨?Ｓｗｉｄ（Ｓ，ｌ〇？〇ｍ?＂｜?｜?Ｒｕｌｅ?ＩＫＵ（?ｈ（ｋ））?ｇ?ｔ？ｋ?￣｜?ｉｄ?０６７８ｃ２ｃ８?ＩＤ?７９ｂ６ｃｃ２２??（ａ）?Ｖｅｒｉｆｉｃａｔｉｏｎ?ｔｒｅｅ?（ｂ）?Ｓｕｂｔｒｅｅ?（ｃ）?Ｍｅｒｇｅｄ?ｔｒｅｅ??圖３．５安全協(xié)議全自動形式化驗證系統(tǒng)構(gòu)建狀態(tài)樹的示例??３．３．２信息收集模塊??１．選擇信息??狀態(tài)樹節(jié)點存儲信息的選擇是系統(tǒng)設(shè)計的重要環(huán)節(jié)。首先，系統(tǒng)將節(jié)點存儲??信息轉(zhuǎn)換為ＤＱＮ的輸入，由于在驗證模塊中系統(tǒng)使用ＤＱＮ在驗證樹中選擇一??個驗證路徑，ＤＱＮ的輸入狀態(tài)需代表當(dāng)前的證明狀態(tài)。因此，節(jié)點信息應(yīng)可以??表示驗證過程中的證明狀態(tài)。由于網(wǎng)絡(luò)難以處理高維數(shù)據(jù)，網(wǎng)絡(luò)輸入的維數(shù)不應(yīng)??太大。所以，系統(tǒng)不選擇驗證過程產(chǎn)生的所有中間數(shù)據(jù)作為節(jié)點信息。其次，系??統(tǒng)使用節(jié)點中的信息來區(qū)分不同的證明狀態(tài)。由于系統(tǒng)逐輪運行，每輪都會構(gòu)造??并合并狀態(tài)樹。在合并過程中，系統(tǒng)需比較不同樹中節(jié)點中的信息，以在不同樹??中找到相同的證明狀態(tài)以完成合并。因此，節(jié)點存儲信息不僅應(yīng)該足夠簡單，而??且在驗證過程中應(yīng)代表獨立的狀態(tài)。??整體上看，Ｔａｍａｒｉｎ在驗證過程中主要生成了如下的中間數(shù)據(jù)：??１．當(dāng)前證明步驟編號：該數(shù)據(jù)用于標(biāo)識當(dāng)前證明狀態(tài)在證明樹中所處的位置，??即從節(jié)點到根的距離。??２．待證明的目標(biāo)：該數(shù)據(jù)用于標(biāo)識當(dāng)前證明狀態(tài)待證明的目標(biāo)。??

ｒｅｃｔ?Ｎｏｄｅ?—＞?Ｚｂ?Ｃ?：?Ｐ（Ａｉ）＜ｌ／２?Ａｉ?Ｂｉ?Ｐ（Ｂｉ）＞ｌ／２??：?ｉｉ＼??Ｄ?Ｅ?］?Ａｎ－２?Ｂｎ－２??Ｂａｃｋｔｒａｃｋｉｎｇ?Ｐｏｉｎｔ??ｎ?：？?「?廠＾一??（ＤＦＳ）?＾Ａ＇?？?Ａｎ－ｌ?Ｂｎ－ｌ??，?：?ｗ??Ｉ?．?Ｄｅｔｅｃｔｅｄ?￣￣?—?￣??Ｄｅｔｅｃｔｅｄ?Ｉｎｃｏｒｒｅｃｔ?Ｎｏｄｅ—＞?Ｄ?Ｇ?？?｜ｎｃｏｒｒｅｃｔ—＞?Ａｎ?Ｂｎ??．?Ｎｏｄｅ??（ａ）?：?（ｂ）??圖３．７狀態(tài)樹：（ａ）第一個不正確的節(jié)點和第一個被檢測到不正確的節(jié)點間存在非零距離??（ｂ）在第一次遍歷后包含正確引理的節(jié)點被選擇的概率??２）本系統(tǒng)使用ＤＱＮ的優(yōu)勢根據(jù)上述定理，系統(tǒng)使用的ＤＱＮ遠(yuǎn)優(yōu)于簡單算??法。通過在每輪中進(jìn)行優(yōu)化，ＤＱＮ可以調(diào)整樹中每個節(jié)點的Ｑ值，并傾向于選??擇具有較高Ｑ值的節(jié)點作為“好的節(jié)點”，其更有可能包含正確引理。例如，在??圖３．７（ｂ）中，假設(shè)ＤＱＮ和簡單算法沿著相同的路徑［４，遍歷，直到正??確性評估算法首次檢測到不正確的節(jié)點。然后，簡單算法從４？開始回溯，并繼??續(xù)沿［Ａｏ，＾，．．．，＾］遍歷。假設(shè)ＡＱ有兩個子節(jié)點。根據(jù)定理，包含正確引理??的概率小于Ｉ即類似地，所有４，Ａ２，…，節(jié)點包含正確引理的??概率呈指數(shù)下降。因此，￡，，成為下一個遍歷的節(jié)點概率較低。相比之下，ＤＱＮ??將節(jié)點Ａ１；Ａ２，…，Ａ？的獎勵設(shè)置為負(fù)值，以使更新后的策略傾向于選擇晃而不??是。實驗評估一節(jié)也對上述分析進(jìn)行了驗證。??３．４實驗評估??３．４．１實驗配置??１．實驗環(huán)境??本章的實驗在裝有?Ｍｅｌ?Ｂｒｏａｄｗｅ


本文編號：3617076