Abstract:
SMV is a tool for checking finite state systems. In this paper, a methodology is presented for using SMV to analyzecryptographic protocols. We illustrate the feasibility of the approach by analyzing Needham-Schroeder Public-Key Protocol and discover thewell-known attack upon the Protocol.
摘要： SMV是分析有限状态系统的一种工具。提出了使用SMV来分析密码协议的方法。为了说明这种方法的可村住，用SMV分析了Needham－Schroeder公钥协议。并成功地找到了对此协议的著名攻击．
关键词:
模型检测,
Needham－Schroeder公钥密码协议,
SMV
CLC Number:
Zhang Yuqing, Zhu Hongru, Xiao Guozhen. Using SMV for Cryptographic Protocol Analysis: A Case Study[J]. , 1999, 25(S1): 156-158.
张玉清,朱宏儒,肖国镇. 密码协议的SMV分析:实例研究[J]. , 1999, 25(S1): 156-158.