基于Petri网的安全协议分析与检测方法的研究

论文摘要

随着Internet技术持续突飞猛进地发展,网络上的信息安全问题日益突出。特别是电子商务、数字货币和网络银行等新业务的深入开展,信息的保密性、完整性和可用性等安全问题成了关键之所在。安全协议,又称密码协议,是以密码学为基础的协议,它在网络和分布式系统中提供各种各样的安全服务。安全协议的目标都与安全有关,例如,认证主体的身份;在主体之间分配会话密钥等。目前,安全协议已广泛应用于计算机网络与分布式系统中,当前关于安全问题的研究热点之一是安全协议的形式化描述与分析。目前安全协议常见的分析方法包括:逻辑方法、模型检测、定理证明等方法,它们都有各自的优点和缺点。本文主要研究以Petri网模型为基础融入其他方法,提出一种新的协议建模及分析检测方法,并使用该新方法对安全协议进行了分析检测,以验证其有效性。本文的主要创新点及研究成果如下:1.提出了一种新的安全协议建模方法,此方法根据通信主体的三态建立的协议模型具有意义明确、便于分析等特点。2.目前国内外很多学者使用petri网分析安全协议时,往往是通过验证协议的不安全状态是否可达,来判断协议的安全性。而本文所提出的方法是从协议的初始状态出发去检测可能存在的攻击。3.在协议分析检测过程中,本文创造性地融入了其他分析方法,构建了各个通信主体分析集。4.本文研究制定了主体分析集更新规则、攻击检测规则。5.本文使用了该新方法对多个经典协议进行分析检测,并找到了可能存在的攻击。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 信息安全概述
• 1.2 安全协议及其研究现状
• 1.3 本文的创新思路及内容安排
• 第二章 安全协议及攻击
• 2.1 安全协议概述
• 2.1.1 密码体制
• 2.1.2 协议的研究与发展
• 2.1.3 安全协议的概念
• 2.1.4 安全协议的分类
• 2.1.5 安全协议的实现目标
• 2.2 常见的针对安全协议攻击
• 2.2.1 攻击者的知识和能力
• 2.2.2 重放攻击
• 2.2.3 协议多回合执行间的攻击
• 第三章 安全协议常见的分析方法
• 3.1 形式逻辑方法
• 3.2 模型检测技术
• 3.3 定理证明方法
• 3.4 基于PETRI网的分析方法
• 3.4.1 Petri网概述及应用
• 3.4.2 安全协议的Petri网分析方法
• 第四章 一种新的协议模型——协议PETRI网（PPN）
• 4.1 基础PETRI网
• 4.1.1 基础Petri网的定义及性质
• 4.1.2 Petri网的一般建模方法
• 4.2 PETRI网的扩展
• 4.2.1 基础Petri网的局限性
• 4.2.2 经扩展的高级Petri网
• 4.3 安全协议的扩展PETRI网模型——PPN
• 4.3.1 PPN的定义
• 4.3.2 基于PPN的安全协议模型的建立
• 4.3.3 基于PPN的NNSK协议模型
• 4.3.4 基于PPN的NNSK协议的一个攻击模型
• 4.4 小结
• 第五章 一种新的安全协议分析与检测方法
• 5.1 方法的提出
• 5.1.1 协议分析的前提假设与攻击者模型
• 5.1.2 分析的主要步骤
• 5.1.3 主体分析集和潜攻击的定义
• 5.1.4 主体分析集的初始化及更新规则
• 5.1.5 攻击的检测及规则
• 5.2 方法的应用简例
• 5.3 小结
• 第六章 使用新方法分析与检测安全协议
• 6.1 WOO-LAM认证协议的分析与检测
• 6.1.1 协议单回合执行模型及检测
• 6.1.2 协议两回合执行的分析与检测
• 6.2 HELSINKI协议的分析与检测
• 6.2.1 协议单回合执行的分析与检测
• 6.2.2 协议两回合执行的分析与检测
• 第七章 结束语
• 7.1 本文的主要研究工作
• 7.2 本文的不足及下一步工作
• 致谢
• 主要参考文献
• 附录