Control Flow Analysis Can Find New Flaws Too
Chiara Bodei, Mikael Buchholtz, Pierpaolo Degano, Flemming Nielson, Hanne Riis Nielson · 2004
A previous study [6] showed how control ow analysis can be applied to analyse key distribution protocols based on symmetric key cryptography. We have extended both the theoretical treatment and our fully automatic veri er to deal with protocols based on asymmetric cryptography. This paper reports on the application of our technique { exempli ed on the Beller-Chang-Yacobi MSR protocol, which uses both symmetric and asymmetric cryptography { and show how we discover an undocumented aw.