The detection of Udpstorm attacks based on model checking linear temporal logic


Citar

Texto integral

Acesso aberto Acesso aberto
Acesso é fechado Acesso está concedido
Acesso é fechado Somente assinantes

Resumo

The intrusion detection based on model checking temporal logic is effective in detecting the complicated and variable network attacks. However, certain types of attacks remain undetected due to the lack of formal models. To solve this problem, a linear temporal logic is employed to model the variable patterns of Udpstorm attacks. First, an analysis of the principles of Udpstorm attacks is given and the details of these attacks are transformed into atomic actions. The atomic actions are then transformed into action sequence. Finally, this type of attacks is expressed in Linear Temporal Logic (LTL) formulas. With the formula thus obstained used as one input of the model checker and the automaton, which expresses the log, used as the other input of the model checker, the results of intrusion detection can be obtained by conducting the LTL model checking algorithm. The effectiveness and the comparative advantages of the new algorithm are verified by the simulation experiments.

Sobre autores

Miaolei Deng

College of Information Science and Technology; Key Laboratory of Grain Information Processing and Control (Henan University of Technology), Ministry of Education

Autor responsável pela correspondência
Email: dmlei2003@163.com
República Popular da China, Zhengzhou, 450001; Zhengzhou, 450001

Kai Nie

School of Information Engineering

Email: dmlei2003@163.com
República Popular da China, Zhengzhou, 450001

Weijun Zhu

School of Information Engineering

Email: dmlei2003@163.com
República Popular da China, Zhengzhou, 450001

Chunyan Zhang

College of Information Science and Technology

Email: dmlei2003@163.com
República Popular da China, Zhengzhou, 450001

Arquivos suplementares

Arquivos suplementares
Ação
1. JATS XML

Declaração de direitos autorais © Allerton Press, Inc., 2017