Control Flow Analysis of Cryptography Protocols Based on Spi Calculus
Han Ji-hong · Jisuanji gongcheng · 2006
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.