Skip to main content

Security protocols, properties, and their monitoring


Andreas Bauer and Jan Jürjens


The Open University


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

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


Served by Apache on Linux on seL4.