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

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

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