针对A(0)协议的新鲜性攻击及改进方案  

A Freshness Attack for A(0) Protocol and Improved Scheme

作　　者：唐郑熠[1] 李均涛[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机技术与发展》2009年第10期164-166,共3页Computer Technology and Development

基　　金：美国GeneChiu基金资助项目(GFC2006-001)

摘　　要：非形式化方法很难保证认证协议的安全性,因此对于形式化方法的研究与应用具有重要的意义,模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A(0)协议进行建模检测的方法,并从检测结果中发现了A(0)协议无法保证公开协商密钥证书新鲜性的缺陷。据此设计出了针对A(0)协议的新鲜性攻击方法,并提出了弥补其新鲜性缺陷的改进方案。由此可见,使用模型检测技术可以高效便捷地对认证协议进行分析。Informal methods are difficult to ensure the security of authentication protoools, so the research and application of the formal methods is very important. The model checking technology is one of the formal methods. Introduce the method of constructing and checking the model of A（0） protocol by SPIN and Promela langnage. From the checking result, we find that A（0） protocol can＇t cnsure the freshness of public agreement key certificate. Hereby the freshness attack for A（0） protocol is designed. Finally, the improved scheme which can make up for the freshness defect is put forward. Thus, it is effieient and convenient to use model checking technology to analyze authentication protocols.

关 键 词：A(0) 新鲜性 协议攻击 模型检测 SPIN PROMELA 

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