基于時(shí)序邏輯模型驗(yàn)證的入侵檢測(cè)方法研究.pdf

1、目前國(guó)際上已實(shí)現(xiàn)的入侵檢測(cè)系統(tǒng)絕大多數(shù)使用模式匹配來(lái)檢測(cè)入侵。隨著網(wǎng)絡(luò)數(shù)據(jù)量的增大，上述系統(tǒng)面臨著一些難以解決的問(wèn)題。為此，一些形式化的方法被提了出來(lái)并被應(yīng)用到入侵檢測(cè)系統(tǒng)中去。其中基于命題線(xiàn)性時(shí)序邏輯(PLTL)的方法即為其中具有代表性的一種，并被證實(shí)可用來(lái)檢測(cè)可變化的復(fù)雜攻擊。然而，基于PLTL的方法與其他相關(guān)方法相比，其綜合性能有哪些優(yōu)勢(shì)與不足，目前尚不清楚，這是本文開(kāi)展研究和解決的問(wèn)題。本文所做的主要工作包括兩個(gè)部分:
　

2、　(1)詳細(xì)分析了誤用檢測(cè)技術(shù)中的模式匹配算法（MPA）和基于模型檢測(cè)的入侵檢測(cè)算法(MCA)。并在KDD99數(shù)據(jù)集的基礎(chǔ)上，構(gòu)造基于行為的入侵檢測(cè)數(shù)據(jù)集，開(kāi)展仿真實(shí)驗(yàn)，從而對(duì)這兩個(gè)算法的檢測(cè)能力、檢測(cè)效率進(jìn)行了比較。
　　(2)提出了一種基于投影時(shí)序邏輯(PTL)的多類(lèi)型攻擊檢測(cè)方法(USA)。該方法主要通過(guò)對(duì)攻擊者、攻擊過(guò)程、攻擊效果建立形式化子模型，利用PTL把子模型結(jié)合起來(lái)，得到多類(lèi)型攻擊的PTL公式模型。將數(shù)據(jù)集和公式模