基于L-學(xué)習(xí)算法的安全協(xié)議自適應(yīng)模型檢測技術(shù)研究.pdf

1、安全協(xié)議是保障網(wǎng)絡(luò)安全的基礎(chǔ)，形式化方法是分析安全協(xié)議是否符合安全目標(biāo)的主流方法。目前對于存在漏洞的協(xié)議，需人為進(jìn)行修正或重新設(shè)計(jì)，這種人工處理方式不僅效率低下，而且嚴(yán)重依賴經(jīng)驗(yàn)、易引入新的漏洞。
　　在網(wǎng)絡(luò)環(huán)境日趨復(fù)雜、通信安全要求日益提高的背景下，將自適應(yīng)技術(shù)引入安全協(xié)議分析，實(shí)現(xiàn)協(xié)議分析與設(shè)計(jì)的一體化、自動化，使安全協(xié)議更具實(shí)效性和安全性，更加適應(yīng)快速變化的新型網(wǎng)絡(luò)環(huán)境和層出不窮的攻擊手段。本文主要研究基于 L*學(xué)習(xí)算法的安

2、全協(xié)議自適應(yīng)模型檢測技術(shù)，主要工作及貢獻(xiàn)包括：
　　1.針對安全協(xié)議及其分析方法，本文對多種形式化方法進(jìn)行了對比分析，并重點(diǎn)研究模型檢測技術(shù)。
　　2.基于經(jīng)典的L*學(xué)習(xí)算法及其改進(jìn)算法，提出一種改進(jìn)的安全協(xié)議自適應(yīng)分析算法。經(jīng)典的L*學(xué)習(xí)算法可以實(shí)現(xiàn)學(xué)習(xí)反例以修正協(xié)議初始模型的功能，但其具有一定的局限性，即要求字符集是有限的，且準(zhǔn)則函數(shù)（teacher）為最小勝任教師（MAT， minimal adequate teach

3、er）。鑒于安全協(xié)議的發(fā)送者、接收者、入侵者以及加密、解密、認(rèn)證等狀態(tài)繁多，在許多應(yīng)用場景MAT不能回答某些成員資格詢問，本文提出一種改進(jìn)的安全協(xié)議自適應(yīng)分析算法，即修正學(xué)習(xí)算法 La*，解決部分教師為缺乏經(jīng)驗(yàn)的問題，并將字符集擴(kuò)展為大字符集。對提出的修正學(xué)習(xí)算法，本文進(jìn)行了正確性證明和復(fù)雜度分析。該修正學(xué)習(xí)算法將有助于提高安全協(xié)議自適應(yīng)模型檢測的效率、降低分析和設(shè)計(jì)成本、緩解狀態(tài)空間爆炸并增強(qiáng)協(xié)議本身對環(huán)境和各種攻擊手段的防御能力。<

4、br>　　3.基于自適應(yīng)模型檢測策略設(shè)計(jì)一種自適應(yīng)形式化建模及分析方案，并對基于L*學(xué)習(xí)算法的安全協(xié)議自適應(yīng)模型檢測框架進(jìn)行仿真實(shí)現(xiàn)，旨在借鑒實(shí)時更新模型的自適應(yīng)技術(shù)將安全協(xié)議的設(shè)計(jì)過程與分析過程統(tǒng)一起來，根據(jù)反例自動修正模型，并以此指導(dǎo)協(xié)議的改進(jìn)和優(yōu)化，從而將協(xié)議的設(shè)計(jì)和改進(jìn)從繁瑣的人為試探中解放出來，實(shí)現(xiàn)真正意義上的自動分析和建模。與現(xiàn)有的分析和驗(yàn)證方法相比，本方案最大的優(yōu)勢在于，當(dāng)驗(yàn)證出協(xié)議漏洞或需求產(chǎn)生變化時，它可以對協(xié)議模型進(jìn)