Security protocols, properties, and their monitoring

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 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 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. Show more