基于有色Petri网的密码协议形式化分析与验证的研究

摘要

密码协议是以密码学为基础以达到密钥分配与身份认证等目的的一种消息交换协议，是实现计算机网络系统安全的关键，在投入使用之前应该保证它是没有缺陷的。然而大量的事实表明，许多密码协议是存在漏洞的，甚至有些在使用多年后才被发现有漏洞。因此，协议的安全性验证是非常重要的。自Dolev和Yao在1981年首次提出了形式化方法分析密码协议以来，在该领域内涌现出了大量的形式化分析和验证方法。这些方法已经成功地发现了许多密码协议中的不安全因素，但这些方法本身仍然存着在很多问题。 密码协议的信息交换过程可以看作是一个进程，由一系列事件的集合和事件前集与后集的行为来确定。于是，密码协议可以被看成一个Petri网，用Petri网模型验证密码协议。自从该方法被提出，已经有很多文献使用此方法验证了密码协议。但是这种方法不可避免地遇到了状态空间“爆炸”问题。 本文在深入研究基于有色Petri网(CPN)模型的密码协议验证的形式化方法的基础上提出了一种更为简化的方法。这种方法首先把带入侵者的CPN模型中的一些变迁序列进行了合并，然后再进行验证。和传统方法相比，这种方法的优点主要体现在： (1)使模型在形式上变得简单了，但描述的信息量并没有减少； (2)简化了求解状态方程的过程； (3)屏蔽掉了一些具体的细节，有助于使协议的设计者从全局角度分析协议的薄弱环节。 本文最后采用这种方法对Woo-Lam协议和Denning-Sacco协议进行了验证，从而证明了这种方法的有效性。

目录

文摘

英文文摘

声明

第一章绪论

1.1课题背景

1.2研究现状

1.3 Petri网模型及其发展历史

1.4论文的主要工作

1.5内容安排

第二章Petri网和高级Petri网

2.1 Petri网简介

2.2 Petri网的基本概念和性质

2.2.1 Petri网的定义、术语和表示方法

2.2.2 Petri网系统的分类

2.3经典Petri网的不足

2.4有色Petri网

2.5本章小结

第三章密码协议

3.1密码学基础

3.2密码协议

3.3密码协议的分类

3.3.1应用密码校验函数(CCF)的认证协议

3.3.2对称密钥重复认证协议

3.3.3无可信第三方的对称密钥协议

3.3.4具有可信第三方的对称密钥协议

3.3.5无可信第三方的公开密钥协议

3.3.6具有可信第三方的公开密钥协议

3.3.7其他协议

3.4密码协议的攻击

3.4.1从密码协议安全性角度讨论攻击

3.4.2常见类型的攻击分类

3.5密码协议的形式化验证现状

3.5.1信念逻辑

3.5.2模型检测

3.5.3定理证明方法

3.5.4 Petri网方法

3.5.5其他方法

3.6本章小结

第四章密码协议验证的有色Petri网方法

4.1基于CPN的密码协议验证方法的步骤

4.2 Woo-Lam协议

4.3基于CPN模型的Woo-Lam协议的分析与验证

4.4协议存在漏洞的原因

4.5本章小结

第五章改进的密码协议验证方法

5.1改进的CPN模型

5.2改进的基于CPN模型的Woo-Lam协议的验证

5.3两种方法的比较

5.4基于CPN模型的Denning-Sacco协议的验证

5.4.1 Denning-Sacco协议

5.4.2用改进的CPN模型验证Denning-Sacco协议

5.4.3 Denning-Sacco协议改进

5.5本章小结

第六章结论与展望

6.1研究总结

6.2下一步展望

参考文献

致谢

攻读硕士期间发表论文

从事科学研究和学习经历的简历