Skip to main content Skip to main navigation


Automating Interactive Protocol Verification

Lassaad Cheikhrouhou; Andreas Nonnengart; Werner Stephan; Frank Koob; Georg Rock
In: Andreas Dengel; Karsten Berns; Thomas Breuel; Frank Bomarius; Thomas Roth-Berghofer (Hrsg.). KI 2008: Advances in Artificial Intelligence. German Conference on Artificial Intelligence (KI-2008), September 23-26, Kaiserslautern, Germany, Lecture Notes in Artificial Intelligence (LNAI), Vol. 5243, ISBN 978-3-540-85844-7, Springer, Berlin, Heidelberg, 2008.


Showing the absence of security hazards in cryptographic protocols is of major interest in the area of protocol security analysis. Standard model checking techniques - despite their advantages of being both fast and automatic - serve as mere debuggers that allow the user at best to detect security risks if they exist at all. In general they are not able to guarantee that all such potential hazards can be found, though. A full verification usually involves induction and therefore can hardly be fully automatic. Therefore the definition and application of suitable heuristics has turned out to become a central necessity. This paper describes how we attack this problem with the help of the Verification Support Environment (VSE) and how we nevertheless arrive at a high degree of automation.