@CONFERENCE\{IMM2003-02111,
    author       = "C. Bodei and M. Buchholtz and P. Degano and F. Nielson and H. Riis Nielson",
    title        = "Automatic Validation of Protocol Narration",
    year         = "2003",
    pages        = "126-140",
    booktitle    = "Proceedings of the 16th Computer Security Foundations Workshop ({CSFW} 03).",
    volume       = "",
    series       = "",
    editor       = "",
    publisher    = "{IEEE} Computer Society Press",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2111-full.html",
    abstract     = "We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed 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 for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure {RPC}."
}