A Hybrid Attack Graph Analysis Method based on Model Checking

Attack graph is an essential tool for the security assessment of industrial Internet systems. Unfortunately, the traditional attack graph mainly focuses on discrete information and cannot handle continuous information such as temperature and humidity. These continuous data represent the states of the industrial Internet and are also indicators of attacks, which should be included in the attack graph. To this end, this paper presents a hybrid attack graph model, which can simultaneously describe the discrete and continuous information of the system. Based on the hybrid attack graph model, a security analysis method is presented. Firstly, the transformation rule from hybrid attack graph to timed automata is established. Secondly, the security attribute of the system is described by sequential logic of continuous interval, and then the model checker TACK is used to complete the analysis of the system. Finally, an example is analyzed and verified by a smart home system to illustrate the method's effectiveness. The method in this paper provides a new idea for attack graph construction and analysis for industrial Internet systems.