扩展基于本地会话的安全协议验证逻辑分析TLS协议

摘要

安全协议是保证网络安全的重要技术之一，但安全协议自身的缺陷，往往会导致很严重的安全问题。如何验证安全协议能否实现其安全目标，成了研究中的热点问题。近年来，导师苏开乐教授提出了一种基于本地会话的安全协议验证逻辑(LLS)，能有效的对协议的安全性进行分析。由于该理论是一个全新的理论，需要对其进行扩展，以使其能分析更多的协议。 传输层安全协议(TLS，transport layer security)是由IETF在SSL3.0的基础上提出的互联网标准，得到了广泛的应用，其安全性的分析有很高的研究价值。 本文针对对称密钥协商协议的分析，在LLS逻辑的基础上进行了扩展。本文在LLS逻辑最核心的(n，1)-secrecy定理中加入了对协商密钥的分析，针对协商密钥协议要认证的安全规范增加了公理，并对扩展的部分做了证明。随后，本文使用扩展后的LLS逻辑分析了TLS协议的安全性。本文首先分析了认证密钥协商协议的实现目标，包括实体认证、密钥认证、密钥确认、消息完整性等，然后针对TLS协议给出了一系列的具体的验证目标，并对这些验证目标进行了验证。TLS协议允许通信双方新建或重用一个会话，本文对这两种情况分别进行了讨论，并将分析的结果和其他人的工作进行了比较，说明了LLS逻辑的TF确性和优点以及扩展后的LLS逻辑在分析这类协议时的有效性。

目录

文摘

英文文摘

第1章引言

第2章安全协议验证

2.1安全协议

2.2安全协议分析的系统模型

2.3安全协议的形式化分析方法

第3章基于本地会话的验证逻辑

3.1加密信息交换模型

3.2安全协议的实例化空间

3.3基于本地会话的验证逻辑

3.4可观察理论

第4章基于本地会话验证逻辑的扩展

4.1对LLS逻辑的扩展

4.2扩展后的(n-1)-Secrecy定理正确性证明

第5章使用扩展的LLS逻辑分析TLS协议

5.1 TLS协议

5.2 TLS协议新建会话时的安全性分析

5.3 TLS协议恢复已有会话时的安全性分析

5.4相关工作比较

第6章总结与展望

6.1 工作总结

6.2 工作展望

参考文献

致谢

原创性声明