网络安全认证协议形式化分析
形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.安全协议的形式化分析正成为国际上的研究热点.用于安全协议分析的逻辑需要对入侵者进行形式化建模,用于刻画入侵者能力.我们运用一种基于算法知识概念的逻辑分析安全协议,入侵者假定使用算法来计算其知识,入侵者的能力也通过对其所使用的算法作适当的限制来获得.运用模型检测器SPIN对TMN协议进行分析,实验结果证明了此方法的有效性,可方便地用于其它网络安全协议验证.
形式化分析 模型检测 安全协议 算法知识逻辑 入侵者模型 网络安全
肖美华 邓宸芳 马小薏 薛锦云 江耘
南昌大学信息工程学院 江西省公安厅公共信息网络安全监察总队 江西师范大学计算机信息学院
国内会议
西宁
中文
66-69
2005-07-01（万方平台首次上网日期，不代表论文的发表时间）