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

VERIFYING SECURITY PROTOCOLS BASED ON SPI CALCULUS

作　　者：郑清雄[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200240

出　　处：《计算机应用与软件》2011年第3期262-264,292,共4页Computer Applications and Software

摘　　要：在安全协议的各种验证方法中,进程代数方法依托完善的进程演算理论得到了很好的应用。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.

关 键 词：安全协议 SPI演算 测试等价 NSSK协议 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]