基于Spin的安全协议形式化验证技术

Formal verification technologis of security protocol based on Spin

针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。

Aiming at the formal verification problem in security protocols, an improved Promela semantic intruder model was used to complete the model checking for key distribution center protocol, to find that it does＇t meet the security property described by LTL（ Linear Temporal Logic） formula, and to get a protocol vulnerability. An improvement program against vulnerability was proposed. A new Promela semantic modeling was put forward for the improved protocol. The improved intruder modeling method reduces the number of states stored in the model checking, thus the model complexity reduces about40%; and reduces the number of transiations, thus the verification efficiency increases about 44%.