網(wǎng)絡(luò)安全認(rèn)證協(xié)議自動(dòng)分析系統(tǒng).pdf

1、網(wǎng)絡(luò)協(xié)議的安全性分析和驗(yàn)證是當(dāng)今計(jì)算機(jī)安全領(lǐng)域中研究的重大課題。協(xié)議安全性分析包括非形式化和形式化兩種方法，形式化方法是安全協(xié)議分析和驗(yàn)證的主要方法。我們以大量的協(xié)議形式化建模研究為基礎(chǔ)，以網(wǎng)絡(luò)安全認(rèn)證協(xié)議為研究對(duì)象，采用模型檢測(cè)技術(shù)，開(kāi)發(fā)了網(wǎng)絡(luò)安全認(rèn)證協(xié)議自動(dòng)分析系統(tǒng)。該系統(tǒng)功能主要是用來(lái)對(duì)認(rèn)證協(xié)議進(jìn)行自動(dòng)建模與驗(yàn)證。本系統(tǒng)分為用戶界面模塊、自動(dòng)分析建模模塊以及自動(dòng)驗(yàn)證模塊。用戶界面模塊為用戶提供了直觀的GUI界面，以可見(jiàn)即可得的方式

2、對(duì)網(wǎng)絡(luò)認(rèn)證協(xié)議進(jìn)行錄入，用這種方式形成系統(tǒng)所接收的原語(yǔ)言——PDL(Protocol Description Language)；自動(dòng)建模分析子模塊設(shè)計(jì)了認(rèn)證協(xié)議的形式化分析算法，對(duì)認(rèn)證協(xié)議進(jìn)行建模與性質(zhì)規(guī)約；自動(dòng)驗(yàn)證子模塊內(nèi)嵌SPIN，對(duì)建模過(guò)程進(jìn)行自動(dòng)驗(yàn)證并返回驗(yàn)證結(jié)果。 本系統(tǒng)完成了對(duì)雙方公鑰類(lèi)型和三方對(duì)稱密鑰類(lèi)型協(xié)議的自動(dòng)建模與驗(yàn)證，并成功地發(fā)現(xiàn)了N-S、Helsinki、TMN等協(xié)議的攻擊漏洞。針對(duì)狀態(tài)爆炸問(wèn)題，本系統(tǒng)