基于串空间的安全协议形式化验证模型及算法

网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议。首先介绍了当前安全协议形式化验证的前沿方向－－串空间理论,随后阐述了基于该理论设计的自动验证模型－－T模型,给出了该模型的算法及描述,并通过验证改进前后的Needham-Schroeder协议来说明T模型的优势。

A Formal Model and Algorithm for Verifying Security Protocols Based on Strand Spaces

Network security is very important in the information era, while the security protocol is one of the key problems of the network security In this paper, a model of strand spaces, a current leading branch of formal automatic verifying, is described in detail Based on the model of strand spaces, a model checker T is designed for the analysis of security protocols When model T is used, the number of reachable states decreases significantly After that, the framework and the algorithm level descriptions of model T are given It is presented and demonstrated with the Needham Schroeder protocol and the Needham Schroeder Lowe protocol