随着信息技术的快速发展,智能建筑成为“互联网+”和建筑行业深度融合的方向和突破口,而网络安全漏洞的爆发式增长、移动互联网、自动控制等新技术的大量应用都给智能建筑引入了新的信息安全风险,越来越多的网络攻击表明智能建筑是不安全的。基于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模型检测工具进行安全性评估和验证,给出改进方案的性能分析。