一个军网身份鉴别协议的形式化分析及修正  

Formal Analysis and Modification of an Authentication Protocol in Military Network

作　　者：刘璟[1] 祝世雄[1] 周明天[2] 

机构地区：[1]中国电子科技集团公司第30研究所,成都610041 [2]电子科技大学计算机科学与工程学院,成都610054

出　　处：《计算机工程与应用》2005年第30期122-124,共3页Computer Engineering and Applications

基　　金：国家973重点基础研究发展规划项目:信息与网络安全体系研究-密钥管理系统(编号:G1999035803)

摘　　要：分别使用形式化分析工具Casper+FDR和OFM C模型检测器对文[1]提出的一个军网身份鉴别协议进行了分析,找到了一个相同的攻击实例。同时指出了文[1]和文[2]中存在的几个谬误。然后对协议进行了修正。形式化验证结果表明修正后的协议是安全的。Respectively using formal analysis tool Casper and OFMC model checker,we analysed an authentication protocol in military network proposed by [1] and found a same attack upon it.At the same time,we also identified several mistakes in [1] and [2].Then we modified this protocol and the results of formal verification upon the modified protocol prove that it is secure as expected.

关 键 词：身份鉴别协议 形式化分析 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]