基于模型檢測和模態(tài)邏輯的Kerberos協(xié)議安全性分析.pdf

1、互聯(lián)網(wǎng)發(fā)展勢不可擋，正日益深刻地改變?nèi)藗兊膶W(xué)習(xí)、工作和生活，甚至影響到整個社會的進(jìn)程。人們逐漸增加了網(wǎng)絡(luò)上的依賴，那么互聯(lián)網(wǎng)上數(shù)據(jù)保護(hù)顯得格外重要。而他們使用的網(wǎng)絡(luò)環(huán)境是開放的、外露的，安全問題必定存在。為保證用戶信息安全，防止入侵者獲取用戶信息，需要設(shè)計可靠有效的安全協(xié)議。安全協(xié)議是解決計算機(jī)安全問題的重要手段，通過計算機(jī)網(wǎng)絡(luò)中的密碼算法手段來達(dá)到密鑰分發(fā)以及認(rèn)證等安全目標(biāo)。然而，協(xié)議可能不安全，安全分析是一個復(fù)雜且困難問題，已將協(xié)議

2、安全性研究視為重點(diǎn)發(fā)展方向。事實(shí)證明，形式化方法是協(xié)議安全性分析更可靠、更有效的最好方式。
　　認(rèn)證是信息安全中特別關(guān)鍵一步，網(wǎng)絡(luò)通訊之前必定先驗證通訊雙方身份。本文以Kerberos協(xié)議為研究對象，采用形式化方法分析Kerberos協(xié)議，所取得研究成果主要有：（1）運(yùn)用模型檢測技術(shù)分析與檢測 Kerberos協(xié)議，驗證得到協(xié)議不安全；（2）分析Kerberos協(xié)議中存在缺陷，提出改進(jìn)后Kerberos協(xié)議；（3）分析GNY推理規(guī)