Modeling and verifying EPC network intrusion system based on timed automata

Nowadays, the EPC network has been gradually popularized to manufacturing intelligent, retailing and logistics. Due to the widespread use of EPC networks, the security problem therefore, becomes particularly important. In order to obtain the proper defense strategy, we propose a modeling method for EPC network intrusion system. First, we describe the network entities in EPC network, and classify them into detected network entities and attacked network entities. Then, we analyze the intrusion for EPC network, and categorize the existing attack methods for EPC network into two categories: atomic attacks and combined attacks. The atomic attacks include vulnerability detection, attack execution, and attack decision. Based on timed automata, we introduce the formal description of the network environment into the modeling of EPC network intrusion system, and thus construct an intrusion model which gives a formal description of attacks. Our intrusion model can represent the time properties, constraints of network environment and intrusion behaviors. Finally, we verify the correctness of our proposed model in terms of the model checking tool UPPAAL, and compare it with other typical attacking models to show the comprehensiveness and integrity of our proposed model. Besides, we change the value of clock parameter, gain the durations of different intrusion actions and use these data to set the defense strategy.