Control Flow Analysis Can Find New Flaws Too

Chiara Bodei, Mikael Buchholtz, Pierpaolo Degano, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    95 Downloads (Pure)

    Abstract

    A previous study showed how control flow 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 verifier to deal with protocols based on asymmetric cryptography. This paper reports on the application of our technique - exemplified on the Beller-Chang-Yacobi MSR protocol, which uses both symmetric and asymmetric cryptography - and show how we discover an undocumented flaw.
    Original languageEnglish
    Title of host publicationProceedings of Workshop on Issues in the Theory of Security (WITS 04)
    Publication date2004
    Publication statusPublished - 2004

    Cite this

    Bodei, C., Buchholtz, M., Degano, P., Nielson, F., & Nielson, H. R. (2004). Control Flow Analysis Can Find New Flaws Too. In Proceedings of Workshop on Issues in the Theory of Security (WITS 04) http://www.imm.dtu.dk/pubdb/p.php?3058