基于PCL的安全协议匿名性形式化分析方法的研究

摘要

目前，大量的安全协议已经被设计出来，如何验证这些协议是否满足声称的安全性是协议设计与分析的一个重要研究领域。为了验证和分析协议的安全性，密码学家提出了不同的基于符号的形式化方法，如模态逻辑，模型检测逻辑，定理证明逻辑。然而大多数形式化方法都集中在协议的认证性和机密性的分析上，且这些方面的研究已经很成熟，而其他安全属性，如匿名性的形式化分析还处在起步阶段。
　　为了进一步完善安全协议形式化分析理论和更好地分析协议的匿名属性，本文提出一种基于协议组合逻辑(PCL)的匿名性分析方法。通过将观察等价思想和PCL理论相结合，提出分析协议匿名性的形式化方法，并且将这种新的形式化方法应用到具体的网络协议中，通过实例分析说明了该方法的可行性和正确性。
　　本文首先阐述了协议形式化分析研究的背景及意义，指出匿名性形式化分析的研究现状和目前存在的一些不足，介绍了安全协议、匿名性和形式化方法的基本概念，并归纳总结了三类常见的形式化方法，详细描述和分析了一种主要的形式化分析方法——PCL模型。
　　其次，针对协议组合逻辑(PCL)缺乏匿名性分析能力的问题，提出一种新的匿名性形式化分析方法。考虑到协议交互过程中涉及到的信息，将PCL中的消息重新定义为三类:明文，密文和组合消息;结合观察者的分析能力，针对以上三类消息，定义了五条消息等价定理，并归纳了消息等价的语义;在消息等价的基础上，结合迹的概念，定义了迹等价语义;并在迹等价定义的基础上，定义了发送者匿名性、接收者匿名性和关系匿名性。
　　最后，为了验证新方法在形式化分析协议匿名性方面的可行性和正确性，本文选用直接匿名认证协议(DAA)作为新方法的应用实例。使用新方法分别对DAA的两个子协议的匿名性进行形式化推理证明，分析结果表明，DAA协议满足匿名性，并验证了新方法的可行性和正确性。

目录

声明

摘要

插图索引

附表索引

第1章 绪论

1．1 研究背景及课题来源

1．2 国内外研究现状

1．3 选题意义

1．4 本文的主要研究工作

1．5 本文的结构安排

第2章 基础知识

2．1 安全协议

2．1．1 安全协议概述

2．1．2 安全协议分类及安全属性

2．2 匿名相关概念

2．2．1 匿名性基本概念

2．2．2 匿名属性分类

2．3 形式化方法的构成

2．3．1 形式化描述

2．3．2 形式化验证

2．4 形式化方法

2．4．1 协议分析的基本假设

2．4．2 模态逻辑方法

2．4．3 模型检测方法

2．4．4 定理证明方法

2．5 本章小结

第3章 PCL模型

3．1 协议组合逻辑概述

3．2 基本的PCL框架

3．2．1 协议的模型化

3．2．2 语法

3．2．3 语义

3．2．4 证明系统

3．3 PCL理论研究现状

3．4 PCL与其他形式化方法的比较

3．5 本章小结

第4章 基于PCL的匿名性形式化分析新方法APCL

4．1 安全假设

4．2 语法

4．3 等价语义

4．3．1 消息等价语义

4．3．2 迹等价语义

4．4 基于等价的匿名框架

4．5 形式化分析DAA协议的匿名性

4．5．1 直接匿名认证协议(DAA)

4．5．2 DAA协议的抽象化表示

4．5．3 DAA-Join协议的形式化分析

4．5．4 DAA-Sign协议的形式化分析

4．6 本章小结

结论与展望

参考文献

致谢

附录A 攻读学位期间所发表的学术论文