A Calculus for Control Flow Analysis of Security Protocols |
Mikael Buchholtz, Hanne Riis Nielson, Flemming Nielson
|
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. |
Type | Journal paper [With referee] |
Journal | International Journal of Information Security |
Year | 2004 Vol. 2 No. 3-4 pp. 145-167 |
Publisher | Elsevier |
Note | Copyright Springer-Verlag. The original publication is available at springerlink.com. |
Electronic version(s) | [pdf] |
BibTeX data | [bibtex] |
IMM Group(s) | Computer Science & Engineering |