基于Spi演算的密码协议的控制流分析

Control Flow Analysis of Cryptography Protocols Based on Spi Calculus

基于Spi演算和控制流分析,提出了一个密码协议的新分析方法。随后利用该方法对Beller-Chang-Yacobi MSR协议进行了分析,通过证明该协议已知的漏洞,说明该方法是正确的,并通过更深入的研究和分析,证明了该协议在并行会话攻击下是不安全的,基于此对该协议进一步改进,改进后的协议是安全的。

Based on the concepts of the Spi calculus and the control flow analysis, a new technique is presented to analyze the cryptographic protocols. Then it uses the technique to analyze the Beller-Chang-Yacobi MSR protocol. The technique is correct by verifying the known flaws, and through the detailed research and analysis, it proofs the protocol is unsecured under parallel session attack. Based on this, it proves the MSR protocol is secure.