密码协议的SPIN建模和验证

为了将模型检测这种强有力的系统验证技术应用于网络协议的安全分析,形式化建模仍然是目前的关键问题和难点所在.本文提出了一种基于高级过程描述语言的建模方法.根据入侵者角色和攻击目标的不同,从入侵者的角度分析协议的运行模式,为每个主体建立过程模型,用模型检测工具进行分析验证.对BAN-Yahalom协议的SPIN分析验证了这种方法的可行性.该方法具有一定的通用性,对其它网络协议的分析有很好的参考价值.

Modeling and Verifying Cryptographic Protocols Using SPIN

In order to use the strong system verfication 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 descriplion 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.