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