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

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