串空间理论在网络安全协议形式化分析中应用

摘要

网络通信的普及和发展使得对网络协议尤其是安全协议的需求日益增长.同时由于安全要求的多样化以及攻击方式的层出不穷使得对于网络安全协议的形式化分析的效率和准确性提出了更高的要求.原有的形式化分析方法通常不可避免地出现状态空间爆炸问题,这使得对于日益增长的网络通信规模下的复杂协议的分析变得十分困难.串空间理论(strand space theory)的出现提供了避免状态爆炸问题、提高协议形式化分析效率的有效方法.用几个简单协议为例说明了如何利用串空间理论有效地进行协议的形式化分析.