摘要
为了将模型检测这种强有力的系统验证技术应用于网络协议的安全分析,形式化建模仍然是目前的关键问题和难点所在.本文提出了一种基于高级过程描述语言的建模方法.根据入侵者角色和攻击目标的不同,从入侵者的角度分析协议的运行模式,为每个主体建立过程模型,用模型检测工具进行分析验证.对BAN-Yahalom协议的SPIN分析验证了这种方法的可行性.该方法具有一定的通用性,对其它网络协议的分析有很好的参考价值.
In order to use the strong system verification technology model checking in the security property analysis of network protocols,formal modeling method is still the critical problem. In this paper, a modeling method based on a high-level process description language is presented According to the categorizing based on intruders' objectives and roles, we analyze the running mode of protocols from the point of view of the intruders, constructing individual process specification for each principal, then verify them using model checking tools. The analysis of the BAN-Yahalom protocol illustrates the feasibility of the approach. This approach has some generality, and provids a good reference for analysis of other network protocols.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2002年第12A期2099-2101,共3页
Acta Electronica Sinica
基金
国家高性能计算基金(No.00215)
