用于安全协议分析的一种新的状态剪枝方法

摘要

Strand空间模型是利用图的形式来描述和分析安全协议的。通过对该模型的研究,总结了已有的状态空间简化技术;研究了如何将认证测试理论应用于安全协议分析中,根据认证测试理论我们得出了一个剪枝定理。研究表明该剪枝定理能够大大减少协议分析中的冗余状态,提高了协议分析的效率。