@ARTICLE\{IMM2004-02841,
    author       = "M. Buchholtz and H. Riis Nielson and F. Nielson",
    title        = "A Calculus for Control Flow Analysis of Security Protocols",
    year         = "2004",
    pages        = "145-167",
    journal      = "International Journal of Information Security",
    volume       = "2",
    editor       = "",
    number       = "3-4",
    publisher    = "Elsevier",
    note         = "Copyright Springer-Verlag. The original publication is available at springerlink.com.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2841-full.html",
    abstract     = "The design of a process calculus for anaysing security protocols is
governed by three factors: how to express the security protocol in a
precise and faithful manner, how to accommodate the variety of attack scenarios, and how to utilise the strengths (and limit the weaknesses) of the underlying analysis methodology.  We pursue an analysis
methodology based on control flow analysis in flow logic style and we
have previously shown its ability to analyse a variety of security
protocols. This paper develops a calculus, LysaNS that allows for much greater control and clarity in the description of attack scenarios, that gives a more flexible format for expressing protocols, and that at the same time allows to circumvent some of the ``false positives{''} arising in previous work."
}