带参性质的形式化描述与证明

摘要

―状态空间爆炸问题一直是验证领域不可避免的难题。在验证的过程中，我们发现有许多带有参数的性质具有可归纳的特性，例如路径的长度，随机数的取值范围，状态空间的个数，通信的步数等。利用归纳特性我们可以把模型检测技术和归纳证明法结合起来使用。本文选择了两个案例对带参数可归纳性质的验证进行了探讨。案例一涉及的是集成电路领域内的逻辑验证，其中提出的终端性质根据路径的长度具有归纳特性。本文在广义符号轨迹赋值（GSTE）已有理论的基础上，提出了终端满足性算法。本文在相关理论基础上证明了终端满足性算法可以利用归纳特性避免一些冗余的计算，降低计算的复杂性。在Round-Robin仲裁器验证的实验中，实验结果表明枚举法的验证时间是终端满足性算法的3.14倍。另一方面，终端满足性算法可以解决GSTE中提出的强满足性算法的一些限制问题。最后本文对终端满足性算法的合理性和完备性给出了证明。
　　案例二涉及的是 RFID系统中安全性和隐私性的研究。随着 RFID技术的广泛应用，消费者的隐私安全受到越来越多人的重视。设计安全的认证协议是一种有效的保护手段。与此同时，认证协议的验证工作也不可忽视。虽已有很多形式化的验证模型，但是每种方法都有些缺点。本文主要介绍了随机图法和归纳法两种方法。随机图法较直观、可以量化分析。但是验证规模较小，如果随机数取值范围较大，计算复杂性会呈指数级增长。归纳法利用归纳的特性，基于密码学中IND-CPA安全性标准设计了RFID系统中的(r,s,t)-隐私性实验。归纳法可以不受随机数、通信步数取值范围的影响。本文在此基础上设计了(r,s,t,)-安全性实验。最后对OSK协议、VOSK协议进行了验证分析，得出结论：OSK协议不能抵抗拒绝服务攻击，也不能够抵抗重放攻击。即OSK协议不满足(r,s,t)-隐私性标准，也不满足(r,s,t)-安全性标准。VOSK协议不能抵抗拒绝服务攻击，可以抵抗重放攻击。即VOSK协议虽不满足(r,s,t)-隐私性标准，但是满足(r,s,t)-安全性标准。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

1.1 研究工作的背景与意义

1.2 形式化验证方法的国内外研究历史与现状

1.3 本文的主要贡献与创新

1.4 本文的结构安排

第二章 形式化分析方法中的相关技术及背景知识介绍

2.1 广义符号轨迹赋值

2.2 RFID系统中认证协议的形式化验证

2.3 本章小结

第三章 广义符号轨迹赋值中的终端满足性

3.1 问题的引入

3.2 终端满足性相关定义

3.3 终端满足性算法

3.4 终端满足性算法的应用

3.5 终端满足性算法合理性的证明

3.6 本章小结

第四章 射频识别中的隐私性与安全性研究

4.1 问题的引入

4.2 RFID系统中安全与隐私问题的相关定义

4.3 RFID系统中协议的形式化验证

4.4 本章小结

第五章 全文总结与展望

5.1 全文总结

5.2 后续工作展望

致谢

参考文献

攻读硕士学位期间取得的成果