@ARTICLE\{IMM2005-03199,
    author       = "C. Bodei and M. Buchholtz and P. Degano and H. Riis Nielson and F. Nielson",
    title        = "Static Validation of Security Protocols",
    year         = "2005",
    pages        = "347-390",
    journal      = "Journal of Computer Security",
    volume       = "13",
    editor       = "",
    number       = "3",
    publisher    = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3199-full.html",
    abstract     = "We methodically expand protocol narrations into terms of a process algebra in order to specify some of the checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols.  Finally, we demonstrate that these techniques suffice to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew Secure {RPC,} Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi {MSR}."
}