Skip to main content

TS

Security protocols, properties, and their monitoring

Authors

Andreas Bauer and Jan Jürjens

NICTA

The Open University

Abstract

This paper examines the suitability and use of runtime verification as means for monitoring security protocols and their properties. In particular, we employ the runtime verification framework intro- duced in [5] to monitor complex, history-based security-properties of the SSL-protocol. We give a detailed account of the methodology, compare its formal expressiveness to prior art, and describe its application to an open-source Java-implementation of the SSL- protocol. In particular, we show how one can make use of runtime verification to dynamically enforce that assumptions on the crypto-protocol implementations (that are commonly made when statically verifying crypto-protocol specifications against security requirements) are actually satisfied in a given protocol implementation at runtime. Our analysis of these properties shows that some important runtime correctness properties of the SSL-protocol exceed the commonly used class of safety properties, and as such also the expressiveness of other monitoring frameworks.

BibTeX Entry

  @inproceedings{Bauer_Jrjens_08,
    publisher        = {ACM Press},
    isbn             = {978-1-60558-042-5},
    author           = {Bauer, Andreas and J\"urjens, Jan},
    month            = may,
    editor           = {{B. D. Win, S.-W. Lee, and M. Monga}},
    year             = {2008},
    title            = {Security Protocols, Properties, and their Monitoring},
    booktitle        = {4th International Workshop on Software Engineering for Secure Systems},
    pages            = {33--40},
    address          = {Leipzig, Germany}
  }

Download

Served by Apache on Linux on seL4.