SPV: Security Protocol Verifier

SPV is a robust Security Protocol Verifier (SPV), which is particularly suitable for automatic verification of complex protocols with an unbounded number of sessions. The current version of SPV can deal with complex message formats with arbitrarily nested encryptions by public, private, shared and hash keys as well as freshly generated keys. Also, SPV can be used to verify complex security properties such as ` Alice observes (knows) Bob observes (knows) Alice said something'. It has been applied to automatically verify a lot of interesting and important properties for quite complex security protocols like Kerberos V5 and the SET purchase phase protocol.

The thoeretical foundations of SPV include the theory of knowledge structure [2] and Logic of Local Sessions (LLS) [1]. The latter is based on a quite natural semantic model called Instantiation Space. Given a protocol and a log file for a principal's message data flow, which is formalized in Cryptographical Message Exchange model (CME), the notion of Instantiation Space is used to identify all the protocol's local runs carried out by the principal.

SPV exploits the advance of SAT techiniques and the underlying computation engine is SBSAT, a famous SAT solver from the University of Cincinnati.


SPV Tool Download

SPV User Manual


Related publications:

[1] Kaile Su, Weiya Yue, Qingliang Chen, Abdul Sattar, and Mehmet A Orgun. Automatic Verification of Complex Security Protocols With an Unbounded Number of Sessions. Techinical Report. PDF 

[2] Kaile Su, Abdul Sattar, Guanfeng Lv, Yan Zhang: Variable Forgetting in Reasoning about Knowledge. J. Artif. Intell. Res. (JAIR) 35: 677-716 (2009)