TMN密码协议的SMV分析  

SMV Analysis of TMN Cryptographic Protocol

作　　者：张玉清[1,2] 王春玲[1,2] 冯登国[3] 

机构地区：[1]中国科学院研究生院信息安全国家重点实验室 [2]中国科学院研究生院国家计算机网络入侵防范中心北京100039 [3]西安工程科技学院计算机学院

出　　处：《计算机研究与发展》2003年第2期258-262,共5页Journal of Computer Research and Development

基　　金：国家自然科学基金 (60 10 2 0 0 460 2 73 0 2 760 2 73 0 2 9)

摘　　要：密码协议安全性的分析是网络安全的一个难题 ,运用形式方法对密码协议进行分析一直是该领域的研究热点 运用模型检测工具SMV对TMN密码协议进行了形式分析 在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上 ,使用SMV对TMN密码协议进行了安全分析It is a hard problem in the area of computer network security to analyze cryptographic protocols Using formal methods to analyze cryptographic protocols remains the key issue in this field In this paper, a methodology is presented by using a model checker of formal methods, SMV, to analyze the TMN cryptographic protocol After building a finite state system of the protocol and describing the security property of the protocol,SMV is used to discover some new attacks upon TMN cryptographic protocol

关 键 词：TMN密码协议 SMV 分析 形式方法 网络安全 密码体制 计算机通信网 移动通信 

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