基于SMV的安全协议模型检验  

Security Protocol Model Checking Based on SMV

作　　者：刘锋[1] 李舟军[1] 李梦君[1] 宋震[1] 张艳[2] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073 [2]四川大学数学学院,四川成都610064

出　　处：《计算机工程与科学》2004年第2期28-31,62,共5页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(90104026);国家863计划资助项目(2002.AA144 040);高等学校重点实验室访问学者基金

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

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

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]