基于Spi演算的安全协议验证

摘要

在安全协议的各种验证方法中,进程代数方法依托完善的进程演算理论得到了很好的应用.Spi演算在PI演算的基础上扩充了密码操作原语来刻画安全协议,并使用测试等价验证安全属性.讨论了利用Spi演算进行验证的过程,并对经典NSSK协议进行分析.%Among several authentication methods for security protocols, process algebra approach which relies on a sound theory of concurrent process calculus has been well applied.The Spi calculus depicts security protocols as an extension of the pi calculus by enriching its cryptographic primitives, and uses testing equivalence to verify security properties.The process of authentication with Spi calculus is discussed in the paper, the analysis on classical NSSK protocol is carried out using this approach as well.