Instantiation Space逻辑在公钥认证协议形式化分析中的应用

摘要

网络的普及为社会生活带来无限便利的同时，其易攻击性也会导致不可估量的后果，如何保障网络安全已是当今开放的网络亟待解决的问题。安全协议是网络安全的有效保障手段之一，而安全协议的可靠性问题受到越来越多的关注。 安全协议形式化分析方法在近30年得到了迅速发展。InstantiationSpace逻辑是苏开乐教授提出的用于安全协议形式化证明方法中的模态逻辑，它将知识推理运用到安全协议形式化分析中，并开发了相应的自动化验证工具SPV。 本文将InstantiationSpace逻辑应用于公钥认证协议的形式化验证中，选取了SPLICE/AS和Denning-Saeco两个典型的公钥认证协议，利用该逻辑系统公理进行了严格、准确地推导和分析，得出了InstantiationSpace在公钥认证协议中对于防止伪装攻击的有效性，同时也指出了该逻辑在验证多重会话攻击上是不完备的。 在进行公理推导的基础上，本文还利用工具SPV对更多的公钥认证协议进行了自动化验证，与协议推导取得了一致的验证结果。通过推导和工具的互补检验，证明了InstantiationSpace逻辑及其工具SPV在公钥认证协议验证中的正确性和可靠性。

目录

文摘

英文文摘

第1章概述

第2章实例化空间

第3章基于Instantiation Space逻辑的公钥认证协议验证

第4章SPV在公钥认证协议中的应用

第5章总结和展望

参考文献

致谢

原创性声明