Security Protocol Model Checking Based on SMV
Yan Zhang · Computer Engineering and Science · 2004
SMV is a symbolic model checking tool based on linear temporal logic. In this paper we verify the Needham-Schroeder protocol by SMV, and finally find out an attack sequence which is achieved by replaying messages.