摘要：SMV是一个基于线性时态逻辑的符号化模型检验工具.本文利用SMV对Needham-Schroeder公钥协议的简化版本进行了验证,发现了利用消息重放进行的攻击.

关键词：smv 安全协议 消息重放 计算机网络 网络安全 

单位：国防科技大学计算机学院; 湖南; 长沙; 410073; 国防科技大学计算机学院; 湖南; 长沙; 410073; 武汉大学软件工程国家重点实验室; 湖北; 武汉; 430072; 四川大学数学学院; 四川; 成都; 610064