TY - GEN
T1 - Security protocols, properties, and their monitoring
AU - Bauer, Andreas
AU - Jürjens, Jan
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
KW - Language-based security
KW - Monitoring history-based properties
KW - Runtime verification
KW - Security automata
KW - Security protocols
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=57049172592&partnerID=8YFLogxK
U2 - 10.1145/1370905.1370910
DO - 10.1145/1370905.1370910
M3 - Conference contribution
SN - 9781605580425
T3 - Proceedings - International Conference on Software Engineering
SP - 33
EP - 40
BT - 30th International Conference on Software Engineering, ICSE 2008 Co-located Workshops - Proceedings of the 4th International Workshop on Software Engineering for Secure Systems, SESS'08
T2 - 30th International Conference on Software Engineering, ICSE 2008 - 4th International Workshop on Software Engineering for Secure Systems, SESS'08
Y2 - 17 May 2008 through 18 May 2008
ER -