NSPK协议的Promela语言建模及分析

Promela modeling and analysis for NSPK protocol

重点提出了对NSPK协议进行建模设计的思想和方法,阐述了如何用Promela语言实现模型的关键技术。使用Spin对该模型进行行为模拟和属性校验,结果既能保证协议的正常执行,也能帮助发现安全缺陷。

This paper puts forward the ideas and methods on the modeling of NSPK protocol.It introduces the key technology and method by using Promela for modeling.The use of ＂Spin＂,which was used to simulate the model and check the attribute,is also discussed in the paper.The result shows that the model can not only guarantee the proper execution of the protocol,but also help to find some security flaws.