Using SMV for cryptographic protocol analysis
Yuqing Zhang, Chunling Wang, Jianping Wu, Xing Li · ACM SIGOPS Operating Systems Review · 2001
SMV is a tool for checking finite state systems. In this paper, a methodology is presented for using SMV to analyze cryptographic protocols. We illustrate the feasibility of the approach by analyzing Needham-Schroeder Public-Key Protocol and discover the well-known attack upon the protocol.