@CONFERENCE\{IMM2004-03058,
    author       = "C. Bodei and M. Buchholtz and P. Degano and F. Nielson and H. Riis Nielson",
    title        = "Control Flow Analysis Can Find New Flaws Too",
    year         = "2004",
    booktitle    = "Proceedings of Workshop on Issues in the Theory of Security ({WITS} 04)",
    volume       = "",
    series       = "",
    editor       = "",
    publisher    = "",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3058-full.html",
    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."
}