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

Automatic Verification for Multi-protocol Attacks by Improving Athena

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析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.