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 (eds.) KI 2008: Advances in Artificial Intelligence volume 5243, Lecture Notes in Artificial Intelligence, Kaiserslautern, Germany, Springer, Berlin, Heidelberg, 2008

Abstract:

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.

Files:

  vse-proverif-ki08.pdf

BibTex:

@inproceedings{ CHEI2008,
	Title = {Automating Interactive Protocol Verification},
	Author = {Lassaad Cheikhrouhou and Andreas Nonnengart and Werner Stephan and Frank Koob and Georg Rock},
	Editor = {Andreas Dengel, Karsten Berns, Thomas Breuel, Frank Bomarius, Thomas Roth-Berghofer},
	BookTitle = {KI 2008: Advances in Artificial Intelligence},
	Year = {2008},
	Series = {Lecture Notes in Artificial Intelligence},
	Publisher = {Springer},
	Publisher = {5243}
}

     
Last modified:: 30.08.2016