论文题目：基于HCPN模型检测方法的BACnet协议形式化安全评估与改进
摘要：随着信息技术的快速发展,智能建筑成为“互联网+”和建筑行业深度融合的方向和突破口,而网络安全漏洞的爆发式增长、移动互联网、自动控制等新技术的大量应用都给智能建筑引入了新的信息安全风险,越来越多的网络攻击表明智能建筑是不安全的。基于TCP/IP技术的数据通信协议被广泛应用于智能建筑系统中,尽管已经实现了对智能建筑设备进行远程监控的要求,但原始的数据通信协议面临着更大的网络攻击威胁。本文以智能建筑协议“BACnet设备认证”为研究对象,以有色Petri网理论和Delov-Yao攻击方法为指导,基于CPN Tools模型检测工具,重点研究该协议的设备认证部分的形式化建模和安全评估,挖掘协议漏洞,提出针对性的安全改进方案,并对所提出的方案应用CPN模型检测工具进行安全性验证。1.基于有色Petri网理论的协议分层建模方法,在建立消息流模型的基础上,基于CPN模型检测工具,建立2层结构的BACnet协议设备认证的HCPN模型,对协议的工作模式和数据传输进行细粒度的建模,精确反映协议运行的细节,根据状态空间分析结果对BACnet协议设备认证模型的功能一致性进行验证。2.充分利用CPN在建模和验证并发、分布式系统和其它系统的方面有较强优势,针对安全协议形式化分析方法中攻击者的强大能力,研究基于改进后的Delov-Yao攻击者模型。在原始的HCPN模型基础上,引入重放、欺骗和篡改三种改进的攻击者模型建立协议的安全评估模型,并基于协议认证属性的形式化定义、CPN模型分析工具和状态空间查询方法评估全攻击状态下的协议的安全性,挖掘BACnet协议设备认证存在的安全漏洞。3.根据协议的安全评估结果和协议漏洞,针对性地提出协议的改进方案,包括密钥分发阶段和身份认证阶段的安全改进。对于密钥分发阶段,主要改变密钥的分发方式,同时引入随机数,保证通信会话密钥不会被攻击者劫持。对于身份认证阶段,主要是添加随机数,保证协议消息不会重放。并对改进方案应用CPN模型检测工具进行安全性评估和验证,给出改进方案的性能分析。
关键词：BACnet;CPN;形式化建模;安全评估;安全改进
学科专业：电子与通信工程（专业学位）
摘要
Abstract
第1章 绪论
1.1 研究背景、意义与课题来源
1.2 BACnet研究现状
1.2.1 BACnet简介
1.2.2 BACnet国内外现状
1.2.3 BACnet前景
1.3 BACnet安全性问题研究现状
1.4 本文的主要研究工作
1.5 本文的结构安排
第2章 相关理论和概念
2.1 BACnet协议
2.1.1 BACnet协议的体系结构
2.1.2 BACnet协议的基本内容
2.1.3 BACnet协议网络安全服务
2.1.4 BACnet和 Internet互连
2.2 Petri网理论基础
2.2.1 Petri网基本概念及特性
2.2.2 有色Petri网
2.2.3 CPN Tools
2.3 攻击者模型
2.3.1 Delov-Yao攻击者模型
2.3.2 协议的攻击分类
2.4 本章小结
第3章 BACnet协议设备认证HCPN建模
3.1 BACnet协议设备认证消息流模型
3.2 BACnet协议设备认证的建模假设和颜色集
3.2.1 建模假设
3.2.2 关键消息和颜色集定义
3.3 BACnet协议设备认证的HCPN模型建立
3.3.1 BACnet协议设备认证的顶层模型
3.3.2 BACnet协议设备认证的实体层模型
3.4 原始模型的功能一致性验证
3.4.1 预期结果分析
3.4.2 状态空间结果分析
3.5 本章小结
第4章 基于攻击者模型的协议安全评估
4.1 改进的Delov-Yao攻击者模型
4.2 协议安全评估模型建立
4.3 安全评估模型的状态空间分析
4.3.1 BACnet协议设备认证安全评估模型的状态空间表
4.3.2 功能一致性分析
4.4 本章小结
第5章 BACnet协议设备认证的新方案
5.1 基于HCPN建模的BACnet协议设备认证安全新方案
5.2 新的BACnet协议设备认证的HCPN模型
5.2.1 改进后的设备认证的CPN顶层模型
5.2.2 改进后的设备认证的CPN实体层模型
5.3 新的BACnet协议设备认证安全评估
5.3.1 新的设备认证的CPN安全评估模型
5.3.2 安全评估模型的状态空间分析
5.4 新方案安全性分析
5.5 新方案性能分析和方案对比
5.6 本章小结
总结与展望
致谢
参考文献