Security protocols, properties, and their monitoring

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 introduced 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 SSLprotocol. 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 ...

• Type: Conference
• Year: 2008
• Where: ICSE
• Authors: Andreas Bauer 0002, Jan Jürjens
• Keywords: ICSE 2008, Runtime Correctness Properties, Runtime Verification, Runtime Verification Framework, Software Engineering