Formal Security Evaluation And Improvement Of BACnet Protocol Based On HCPN Model Detection Method

With the rapid development of information technology,smart buildings have become the direction and breakthrough point for the deep integration of “Internet +” and the construction industry.The explosive growth of network security vulnerabilities,the large number of new technologies such as mobile Internet and automatic control have all introduced smart buildings.New information security risks.An increasing number of cyber attacks indicate that smart buildings are not secure.Data communication protocols based on TCP / IP technology are widely used in intelligent building systems.Although the requirements for remote monitoring of intelligent building equipment have been implemented,the original data communication protocols are facing greater threats from network attacks.In this thesis,the intelligent building protocol “BACnet equipment certification” is taken as the research object,and the colored Petri net theory and the Delov-Yao attack method are used as guidance.Based on the CPN Tools model detection tool,this paper focuses on the formal modeling and security of the equipment certification part of the protocol Evaluate,mine protocol vulnerabilities,propose targeted security improvement solutions,and apply CPN and Scyther model monitoring tools to the proposed solutions for security verification.1.A protocol layered modeling method based on colored Petri net theory.Based on the establishment of the message flow model,based on the CPN model detection tool,a HCPN model of the BACnet protocol device authentication with a 2-layer structure is established.Fine-grained modeling,which accurately reflects the details of protocol operation,and verifies the functional consistency of the BACnet protocol device authentication model based on the results of state space analysis.2.Taking full advantage of CPN in modeling and verifying concurrency,distributed systems,and other systems,it has strong advantages.In view of the powerful capabilities of attackers in formal analysis methods of security protocols,the research is based on the improved Delov-Yao attacker model.Based on the original HCPN model,three improved attacker models including replay,spoofing,and tampering are introduced to establish a protocol security evaluation model.Based on the formal definition of the protocol's serious attributes,CPN model analysis tools,and state space query methods,the security of the protocol in the full attack state is evaluated,and the security loopholes in the BACnet protocol device authentication are discovered.3.According to the security evaluation results and protocol loopholes of the protocol,specific improvements to the protocol are proposed,including security improvements in the key distribution phase and the identity authentication phase.For the key distribution phase,the key distribution method is mainly changed,and random numbers are introduced to ensure that the communication session key will not be hijacked by the attacker.For the authentication phase,random numbers are added to ensure that protocol messages cannot be tampered with.The safety evaluation and verification of the improved scheme using the CPN model detection tool is given,and the performance analysis of the improved scheme is given.