改进Athena算法的多协议攻击自动化验证方法  

Automatic Verification for Multi-protocol Attacks by Improving Athena

作　　者：刘威[1,2] 郭渊博[1,2] 雷新锋[3] 李俊锋[4] 

机构地区：[1]解放军信息工程大学 [2]数学工程与先进计算国家重点实验室 [3]中国人民解放军第61840部队 [4]太原卫星发射中心

出　　处：《计算机科学》2014年第12期112-117,132,共7页Computer Science

基　　金：国家部委基金项目(9140C130103120C13062)资助

摘　　要：多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议交互消息和计算生成当前协议消息的能力,能够以自动化的方式验证协议是否存在多协议攻击。实验结果表明,提出的方法能够实现多协议攻击的自动化验证。Protocol security in multi-protocol environments is an open issue in formal analysis for security protocols.Aiming at this problem,an automatic verification for multi-protocol attacks was proposed based on Athena algorithm.The state representation and successor state generation algorithm of Athena are extended,and the attacker can intercept messages from one protocol and insert messages generated by it to another protocol.Some state reduction rules are introduced.The method can verify whether there is a multi-protocol attack.The experiment results show that the method can implement automatic verification for multi-protocol attacks.

关 键 词：多协议攻击 自动化验证 安全属性 Athena算法 逆向搜索 

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