Intrusion detection based on model checking timed interval temporal logic

2010 ◽  
Author(s):  
Weijun Zhu ◽  
Qinglei Zhou ◽  
Ping Li
Keyword(s):  
Model Checking ◽  
Intrusion Detection ◽  
Temporal Logic ◽  
Interval Temporal Logic

A Novel Approach for Intrusion Detection Based on Model Checking Interval Temporal Logic with Past Construct

2014 ◽  
Vol 680 ◽  
pp. 451-454
Author(s):  
Peng Zhe Qiao ◽  
Wei Jun Zhu
Keyword(s):  
Model Checking ◽  
Intrusion Detection ◽  
Temporal Logic ◽  
Pattern Matching ◽  
New Method ◽  
Network Attacks ◽  
New Model ◽  
Interval Temporal Logic ◽  
Novel Approach ◽  
Attack Models

Compared with the Intrusion Detection (ID) based on pattern matching, the model-checking-based methods can find the complex attacks. But their rates of missing report are still high. To solve this problem, we firstly use the Interval Temporal Logic with Past Construct (ITLPC) formulae to describe some signatures for network attacks. And then, we can use some automata to establish models of audit logs. On the basis of it, automata, i.e., attack models, and ITLPC formulae, i.e., signatures, constitute the two inputs of the ITLPC model checking algorithm. Therefore, a new model-checking-based ID algorithm is obtained by calling the ITLPC algorithm. Compared with the existing methods, the new method is more powerful, as shown in the experimental simulations.

Intrusion Detection for Universal Attack Mode Based on Interval Temporal Logic with Past Construct

2014 ◽  
Vol 1006-1007 ◽  
pp. 1047-1050
Author(s):  
Yong Liang Li ◽  
Wei Jun Zhu ◽  
Qing Lei Zhou
Keyword(s):  
Model Checking ◽  
Intrusion Detection ◽  
Temporal Logic ◽  
Pattern Matching ◽  
Detection Method ◽  
Semantic Relation ◽  
New Method ◽  
Interval Temporal Logic ◽  
Universal Relationship ◽  
Set Up

Compared with the intrusion detection based on pattern matching, the method which is based on model checking can detect the complex attacks. But all of the existing algorithms are used to detect some specific types of attacks. So, we firstly use the Interval Temporal Logic with Past Construct (ITLPC) formulae to set up formal sub-models respectively for the five kinds of attackers, the four kinds of attack processes and the eight kinds of attack effects. According to their universal relationship and the semantic relation of variety of ITLPC logic operators, we obtain the above sub-models together, thus, the universal models described by ITLPC formulae for universal attacks are formed. On this base, we implement an intrusion detection method based on ITLPC for detecting all types of attacks. Compared with the existing methods, the detecting ability of the new method is more comprehensive.

scholarly journals A Novel Algorithm for Intrusion Detection Based on RASL Model Checking

2013 ◽  
Vol 2013 ◽  
pp. 1-10 ◽  
Author(s):  
Weijun Zhu ◽  
Qinglei Zhou ◽  
Weidong Yang ◽  
Haibin Zhang
Keyword(s):  
Model Checking ◽  
Intrusion Detection ◽  
Real Time ◽  
Temporal Logic ◽  
Timed Automata ◽  
Expressive Power ◽  
Detection Methods ◽  
Time Interval ◽  
Detection Systems ◽  
Interval Temporal Logic

The interval temporal logic (ITL) model checking (MC) technique enhances the power of intrusion detection systems (IDSs) to detect concurrent attacks due to the strong expressive power of ITL. However, an ITL formula suffers from difficulty in the description of the time constraints between different actions in the same attack. To address this problem, we formalize a novel real-time interval temporal logic—real-time attack signature logic (RASL). Based on such a new logic, we put forward a RASL model checking algorithm. Furthermore, we use RASL formulas to describe attack signatures and employ discrete timed automata to create an audit log. As a result, RASL model checking algorithm can be used to automatically verify whether the automata satisfy the formulas, that is, whether the audit log coincides with the attack signatures. The simulation experiments show that the new approach effectively enhances the detection power of the MC-based intrusion detection methods for a number of telnet attacks, p-trace attacks, and the other sixteen types of attacks. And these experiments indicate that the new algorithm can find several types of real-time attacks, whereas the existing MC-based intrusion detection approaches cannot do that.

Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments

2016 ◽  
pp. 389-405 ◽  
Author(s):  
Laura Bozzelli ◽  
Alberto Molinari ◽  
Angelo Montanari ◽  
Adriano Peron ◽  
Pietro Sala
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Interval Temporal Logic ◽  
Logic Model Checking

Model Checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic

2012 ◽  
Vol 198-199 ◽  
pp. 889-893
Author(s):  
Hai Bin Zhang ◽  
Li Ya Yang
Keyword(s):  
Model Checking ◽  
Hybrid Systems ◽  
Temporal Logic ◽  
Desirable Property ◽  
Interval Temporal Logic

This paper investigates the model checking issue of multirate hybrid systems. To this end, multirate automata are used to represent the possible behavior of multirate hybrid systems, and a dense timed interval temporal logic (DTITL) is defined to describe the desirable property. To check whether a multirate automaton satisfies a DTITL formula, a corresponding region automaton and a propositional interval temporal logic (PITL) formula are constructed. After each vertex of the region automaton being labeled with propositions appearing in the corresponding PITL formula, the model checking problem for mutirate hybrid systems is reduced to the same issue for PITL, which can be solved readily.

scholarly journals Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

2019 ◽  
Author(s):  
Jakub Michaliszyn ◽  
Piotr Witkowski
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Order Logic ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Interval Temporal Logic ◽  
Multi Agent ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

Sign in / Sign up

Export Citation Format

Share Document