|
|||||
|
|
| 网络安全认证协议形式化分析 | |
| 作者姓名： | 肖美华 江耘 邓宸芳 马小薏 薛锦云 |
| 作者单位： | 南昌大学信息工程学院;江西省公安厅公共信息网络安全监察总队;江西师范大学计算机信息学院 |
| 基金项目： | 国家重大基础研究(973计划)前期研究专项项目(2003CCA02800)，江西省自然科学基金资助项目(0411041)，江西省教育厅科技计划项目(GrantNo.200543)，南昌大学2003、2004年度科研基金项目 |
| 摘 要： | 形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。安全协议的形式化分析正成为国际上的研究热点。用于安全协议分析的逻辑需要对入侵者进行形式化建模,用于刻画入侵者能力。我们运用一种基于算法知识概念的逻辑分析安全协议,入侵者假定使用算法来计算其知识,入侵者的能力也通过对其所使用的算法作适当的限制来获得。运用模型检测器SPIN对TMN协议进行分析,实验结果证明了此方法的有效性,可方便地用于其他网络安全协议验证。 |
| 关 键 词： | 形式化分析 模型检测 安全协议 算法知识逻辑 入侵者模型 SPIN/Promela |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |