摘要
形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。安全协议的形式化分析正成为国际上的研究热点。用于安全协议分析的逻辑需要对入侵者进行形式化建模,用于刻画入侵者能力。我们运用一种基于算法知识概念的逻辑分析安全协议,入侵者假定使用算法来计算其知识,入侵者的能力也通过对其所使用的算法作适当的限制来获得。运用模型检测器SPIN对TMN协议进行分析,实验结果证明了此方法的有效性,可方便地用于其他网络安全协议验证。
出处
《计算机安全》
2006年第2期36-38,共3页
Network & Computer Security
基金
国家重大基础研究(973计划)前期研究专项项目(2003CCA02800)
江西省自然科学基金资助项目(0411041)
江西省教育厅科技计划项目(GrantNo.200543)
南昌大学2003
2004年度科研基金项目