包含XOR的安全协议自动验证的改进

摘要

安全协议通常描述了公共网络中两个或多个智能进程之间的消息交换行为，从而保证对交互过程中诸如认证、机密保持、密钥一致、隐私和匿名性等安全属性的支持。但是，设计一个安全可信的协议并不是一件容易的事情，而这些不安全的协议往往就系统攻击的入口点。从Lowe[1]提出了形式化自动验证之后，该验证方法已经展示了其在协议安全性证明方面的强大优势并得到了广泛的应用。
　　 由于针对密码学原语具体算法的攻击往往难以分析，以自动化的形式证明攻击就更加困难，因此密码学操作原语在形式化验证中往往被看作是不带任何代数属性的函数符号，忽略其具体计算细节，这个假设被称为完美密码假设证[2]，也就是说加密后的消息除非使用相应的密钥解密打开，否则是不可能通过其他方式得到其对应明文的。基于这个假设，目前存在很多自动化验证工具，其中ProVerif[3]以其高效的性能被公认为目前最优秀的验证工具之一[4]。但是，ProVerif等上具没有涵盖那些利用密码学操作原语代数属性的攻击。因此，完美假设的限制需要适当放宽，从而将此类攻击有效的识别出来。
　　 位运算符XOR(exclusive or)广泛应用于最近几年流行的RFID协议中，再加上其简洁的格式，已经成为目前的研究热点。因此，为了能够更加有效的发现包含有XOR安全协议的攻击隐患，需要将对操作符代数属性的使用能力加入到入侵者的攻击能力中。
　　 特里尔大学的Kusters教授和Truderung最近提出了一个对包含有操作符XoR(O）安全协议的自动验证方法。在该方法中，包含有XOR的协议模型被自动转换为相应的可进行形式化验证的等价模型，其中已经包含了对XOR的代数属性运算的合理建模，该等价模型可以作为ProVerif的输入模型，由它自动验证。虽然该方法在验证机密性时表现出较高效率但是在认证属性的验证中往往效率不高，对某些协议甚全无法处理。
　　 本文中，针对Kusters和Truderung算法存在的缺陷，提出了两个改进方向：第一，为了扩展可验证认证属性的安全协议的范围，提出了有界验证的方法，使更多的XOR安全认证协议得到自动的有效证明：第二，为了提高该算法的效率，提出了一系列的优化方案，进一步减小转换后的协议模型的规模，缩短ProVerif的验证时间。通过设计实现测试模型，测试了常用的XOR协议标准和若干最新提出的RFID协议。实验结果表明木文提出的改进方案达到了预先的设想效果，并且在实验中发现了在一个RFID协议上新的攻击过程。

目录

文摘

英文文摘

TABLE OF CONTENTS

第1章 绪论

1.1 课题提出的背景和意义

1.2 协议的自动验证

1.3 包含XOR的安全协议

1.4 对包含XOR安全协议验证的研究现状

1.5 研究动机以及贡献

1.6 论文组织框架

第2章 协议验证背景介绍

2.1 协议的描述

2.2 安全属性

2.2.1 机密性

2.2.2 认证属性

2.3 Term Algebra

2.4 利用Hom理论建模安全协议

2.5 Horn理论协议建模实例

2.5.1 机密性验证建模

2.5.2 认证属性验证建模

2.6 ProVerif基木原理

2.7 XOR约简

2.8 木章小结

第3章 认证属性的有界验证

3.1 模型的多会话转换

3.2 正确性证明

3.3 木章小结

第4章 XOR约简算法优化

4.1 基于nonce随机性的优化

4.2 基于会话次序的优化

4.3 基于机密的认证属性验证优化

4.4 针对RFID协议的特殊优化

4.5 基于XOR规则的约简优化

4.6 木章小结

第5章 验证上具实现

5.1 设计目标与框架

5.2 MST-fresh

5.3 MST-general

5.4 MST-RFID

5.5 基于+规则的优化实现

5.6 木章小结

第6章 实验分析

6.1 机密性验证优化实验

6.1.1 验证协议标准

6.1.2 机密性优化验证实验结果

6.2 对认证属性有界验证优化的实验

6.2.1 验证协议标准

6.2.2 认证属性验证实验结果

6.3 本章小结

第7章 总结和展望

7.1 有界验证

7.2 验证效率优化

7.3 展望

参考文献

致谢

攻读学位期间发表的主要学术论文目录

学位论文评阅及答辩情况表