基于串空间理论的安全协议自动验证

来源：计算机应用杂志2015年第7期北京时间：

作者：刘家芬

单位：1. 西南财经大学 经济信息工程学院, 成都 610054;2. 西南财经大学 四川省金融智能与金融工程重点实验室, 成都 610054

摘要：针对目前串空间理论依赖分析人员主观判断、无法使用自动化工具进行验证的问题,提出了基于串空间理论的协议认证属性标准化验证过程。首先为协议消息项定义类型标签,对串空间及认证测试理论进行扩展;然后通过判断测试元素出现位置、检验测试元素参数一致性、确认变换进行边唯一存在性和检验目标串参数一致性,将基于串空间理论的协议验证过程标准化为可程序实现的步骤。该算法的时间复杂度为O(n2),避免了模型检测方法的状态空间爆炸问题,并在此基础上实现了安全协议认证属性的自动化验证工具。以BAN-Yahalom协议和TLS 1.0握手协议为例进行了标准化的分析验证,找到了对BAN-Yahalom协议的一种新攻击形式。该攻击无需限制服务器对随机数的检查,比Syverson发现的攻击更具普遍性。

关键词：串空间,认证测试,安全协议,自动化验证,认证属性,BAN-Yahalom协议,安全传输层握手协议

基金资助：国家自然科学基金重大项目(91218301);国家自然科学基金青年项目(60903201);中央高校基本科研业务费研究项目(JBK20505, JBK140129)。