基于SVO邏輯的網(wǎng)絡安全協(xié)議形式化分析.pdf

1、SVO邏輯已成功分析了NSSK協(xié)議、NSPK協(xié)議、Otway-Rees協(xié)議、Yahlom協(xié)議、大嘴青蛙協(xié)議等，并找到了其中已知的和未知的漏洞。在SVO成功分析的協(xié)議當中大都是基礎性的原始協(xié)議，并且這些協(xié)議在目前計算網(wǎng)絡通訊中逐漸失去其利用價值。面對眾多的安全協(xié)議，不少研究人員已經(jīng)作了大量的工作，但這些分析遠遠不能滿足安全的需求。
　　本文利用SVO邏輯對部分網(wǎng)絡通信和安全協(xié)議進行分析和改進，并針對改進后的SNMP協(xié)議開發(fā)出 Tra

2、p批量設置工具。所做的具體工作如下：
　　1.分析對了稱密碼體制、公鑰密碼體制、數(shù)字簽名等基本算法，并進一步討論了具有代表性的認證協(xié)議，密鑰管理和分配的方法等；分析各類形式化分析方法，并重點對 SVO邏輯進行了分析和討論。
　　2.對 SVO邏輯的推理規(guī)則提出擴展，指出3G通信的認證協(xié)議和密鑰分配協(xié)議（AKA協(xié)議）存在的漏洞并從形式化的角度對該進行了分析和改進做了改進，并運用擴展的SVO邏輯分析了AKA協(xié)議。
　　3.

3、分析了SNMP（簡單網(wǎng)絡管理協(xié)議）主要的缺點，對該協(xié)議通過增添時間戳、對稱密鑰和加密密鑰的方式進行了改進，增強了其認證性和保密性；首次對 SNMP協(xié)議作了形式化描述，并運用SVO邏輯對改進后的SNMP協(xié)議作了形式化分析。
　　4.利用Visual C++6.0、SNMP C++開發(fā)包開發(fā)出基于SNMP協(xié)議的實用性管理工具——Trap批量設置工具。并對將改進前后的SNMP協(xié)議實現(xiàn)結果進行了比較，用實例證實了改進后的SNMP協(xié)議的有效