本文是一篇楼宇自控论文，本文的研究对象是楼宇自控协议“BACnet/IP设备认证机制”，在有色Petri网理论和Dolev-Yao攻击方法指导下，主要从如何正确对该协议设备认证机制进行形式化建模和基于改进的Dolev-Yao攻击者模型建立安全评估模型方面做了详细研究。
第1章绪论
1.1研究背景及意义
随着科技生产力的不断发展和城镇化建设进程的逐渐推进，人们在建筑的建设和优化方面的关注度持续上升。为了发展和完善周围建筑，人们不断将新技术引入应用到建筑领域，想要借助现代科技手段来完成对建筑设备的自动化、智能化管理。智能建筑(Intelligent Building，IB)就是传统建筑与通信技术、自动化控制技术等现代科技方法深度融合而成的一种新型技术产物。它是在楼宇自动化技术的基础上提出的，其目的就是为了能够更好地满足人们对于美好便捷生活的追求以及稳定高效工作的需求。目前越来越多的建筑设备在智能化和功能复杂化水平上得到了快速提升，为了将这些建筑设备的功能更好的发挥出来，提高整个系统对建筑智能设备的控制操作和运维能力，楼宇自动化系统(BAS)一直在融合先进的现代信息通信技术和自动化技术来完善优化自身[1]。
在以往的楼宇自动化系统行业中，传统的厂商开发的系统都是单独封闭的，这完全是因为当时建筑市场规模小、功能要求低、设备类型少等原因造成的。由于这些系统属于厂商内部自主研发，因此其中无论是外在的设备仪表结构、安装方法、信号处理还是内部的网络数据通信协议、数据格式等都只有开发者知晓，对于其他人来说就是黑盒一般的存在。但随着市场需求的快速增加，公众对于智能建筑系统提出了更高的要求，这种不透明的开发方式所存在的问题愈加明显，就好像独立开发系统的厂家所生产的设备因其内部所用协议不同不能完成数据共享工作、设备无法通用不可互换互操作、信息系统集成困难、系统运维成本过高等。因此，市场需求决定了现代楼宇自动化系统必须按照统一的开放技术标准进行开发。针对以上情况，一些国际专业组织和专家开始对楼宇自控系统中数据通信协议的数据格式和传输机制制定统一的约束和标准。
1.2国内外研究现状
1.2.1楼宇自控系统发展现状
上个世纪八十年代初期，我国在楼宇自控系统方面的研究才刚刚起步，这一时期的系统功能还十分简单，仍处在萌芽阶段。到了九十年代中后期，信息系统集成技术的突飞猛进以及计算机、互联网的逐渐普及加快了楼宇自控系统的发展进程，为其奠定了坚实基础[8]。进入二十一世纪后，楼宇自控系统因其具有监控管理便捷以及能够大幅降低能源损耗等特性而受到业界广泛关注并得以快速发展，在此期间产生了一体化集成管理系统。但由于当时市场缺乏统一规范，各个子系统的厂商为了获取更多的利润，同时也为了快速便捷的生产，使用的都是企业内部自主开发的私有协议[9]。这种高度封闭的私有协议不仅给系统集成增加了不小的难度也严重影响了系统间的联通性和互操作性。相比于西方发达国家，各厂商使用封闭不透明的私有协议现象是导致我国楼宇自控系统发展缓慢的根本原因。我国在楼宇自控系统方面还有许多有待发展和完善的地方。
与国内不同的是，楼宇自控系统在国外的发展历史已超过四十年，大致可将其分为以下四个阶段：
(1)中央监控系统
从上个世纪七十年代起，计算机发展到了第四阶段。由于大规模集成电路计算机的广泛应用，楼宇自动化系统的控制方式也因此发生了较大的改变。从这一阶段开始，系统以电子计算机作为中央操控站，按照系统内部设定好的程序对各个采集站的数据信息进行操作，保持设备的自动运行。
(2)集散控制系统
从上个世纪七十年代末到八十年代之间，微处理器技术日益成熟，技术上的提升让楼宇自控系统的功能被划分为四大层级：现场设备级、操作分站级、中央监控主站级和系统管理级[10]。中央监控主站对各个分站进行监控，而各层级分站相互之间又各自独立并且能够单独进行计算和操作。
第2章相关理论知识
2.1 BACnet/IP协议概述
随着信息技术的不断发展和人们对现代化的居住、办公环境的不断追求，智能建筑对楼宇自控系统的远程操控性能提出了更高的要求。对于目前的楼宇自控系统来说，远程监控能力、设备互操作能力、网络通信能力、系统之间的互联互通能力是持续不断提升BAS性能的突破方向。这四大能力的提升必须依靠BACnet标准的内容与互联网的TCP/IP标准进行融合和扩展才能得以实现[47]。
为了使BACnet协议能够与互联网进行联通，1999年BACnet标准定义了一个新的与IP协议融合的互联协议叫做BACnet/IP协议。作为BACnet协议标准的补充，使用BACnet/IP协议通信的楼宇自控系统可以实现不受地域限制地通过互联网对BAS的监控对象进行实时监控和操作[48]。
2.1.1 BACnet/IP协议体系结构
目前在楼宇自控系统领域中应用最为广泛的数据通信协议就是BACnet协议。但是为了满足系统扩展以及方便设备管理与控制等需求，将BACnet网络与IP网络进行融合，实现设备、平台及系统间的互联互操作就显得极为必要了。目前BACnet标准想要实现IP网络与BACnet网络的连接共有两种技术方法可供选择：一种是PAD技术，另一种就是BACnet/IP技术[49]。
2.2协议形式化分析
当前在针对安全协议进行分析研究的各类方法中，协议形式化分析是效果最理想的一种。协议的形式化分析方法总的来说就是利用形式化描述语言对协议主体、消息交互过程以及攻击者的行为进行抽象描述并借助一定的建模工具进行建模分析。其具体的分析操作过程可以分为以下几步：
(1)首先对协议消息交互的过程进行详细的分析总结；
(2)利用形式化描述语言对协议中所涉及的参与实体、消息交互机制等进行抽象性描述；
(3)根据上述描述，选定形式化建模工具对协议进行建模；
(4)在协议模型中根据实际需要添加攻击者模型，并将协议、环境、攻击者作为一个系统整体进行建模；
(5)通过使用形式化的、抽象的、基于数学模型的方法对协议进行安全性分析，从而验证协议在实际应用中是否能够完全满足标准规范中指定的安全属性[53]。
而在本文中所指协议都是处于网络通信领域的，其定义是为了更加规范地进行数据交换而建立的规则或标准的集合，而安全协议则是指能够保障通信安全的机制和规则。安全协议的本质就是通过提供各种安全服务来实现在协议上设定的各种安全目标，以此提高通信的安全性。安全协议通常都是依靠自己设计的密码算法来实现密钥分配、身份认证以及安全属性的验证[54]。
第3章基于设备认证机制的HCPN建模.........................20
3.1构建设备认证机制消息流模型........................20
3.2协议设备认证机制的建模假设和相关颜色集定义........................22
第4章基于攻击者模型的协议安全评估..........................29
4.1改进的Dolev-Yao攻击者模型...........................29
4.2构建协议安全评估模型.................................30
第5章设备认证机制的改进方案.............................34
5.1基于HCPN建模的设备认证机制改进方案.........................34
5.2改进后设备认证机制的HCPN模型............................35
第5章设备认证机制的改进方案
5.1基于HCPN建模的设备认证机制改进方案
根据对协议安全评估模型状态空间报告的分析可知，BACnet/IP协议设备认证机制并不具备抵御欺骗、篡改、重放等中间人攻击的能力。对上述安全威胁，本文提出了一种引入时间戳和生成随机数的方式加强设备认证安全强度的新方案。新方案在设备认证的整个消息交互过程中都加入了时间戳并在实体接收消息时设立了安全阈值，在设备认证阶段则是加入了生成随机数来保证消息不被篡改和重放。新方案中协议的认证消息流(MSC)模型如图5.1所示，其中timestamp是添加到消息中的时间戳信息，Rn则是用于加强认证的生成随机数。
总结与展望
本文的研究对象是楼宇自控协议“BACnet/IP设备认证机制”，在有色Petri网理论和Dolev-Yao攻击方法指导下，主要从如何正确对该协议设备认证机制进行形式化建模和基于改进的Dolev-Yao攻击者模型建立安全评估模型方面做了详细研究。本文的研究工作对于BACnet/IP协议安全性的提升和楼宇自控系统通信安全的建设都具有重要的指导意义和实用价值。本文具体的研究内容和创新如下：
1.通过对协议的设备认证过程进行详细分析，构建出消息流模型图。依照构建的模型图，利用CPN Tools建立原始BACnet/IP协议设备认证机制模型。其中的顶层模型对设备认证机制进行了抽象描述，底层模型对协议运行中数据传输的过程进行了详细描述。通过将模型的状态空间分析结果与协议设备认证机制标准定义对照，验证所建模型是否正确。
2.模型状态空间爆炸一直是协议安全形式化分析建模过程中引入攻击者时的重点关注问题。充分利用CPN Tools在图形化建模和状态空间检测方面的优势，在传统Dolev-Yao攻击者模型基础之上提出了一种改进模型。改进的攻击者模型通过设定的消息分解组合规则以及利用弧表达式和攻击函数代替复杂繁多的库所、变迁来表示不同攻击方法，不仅对攻击过程做到了详细精确的还原，还通过减少库所、变迁的使用降低了模型状态空间生成的计算难度和大小，可以有效的解决状态空间爆炸问题。在基础模型的两层结构之上新增一层，将改进后的攻击者模型加入其中，借此建立协议的安全评估模
