Open Systems Laboratory at Illinois

A temporal logic based framework for intrusion detection

By Prasad Naldurg, Koushik Sen, and Prasanna Thati. In FORTE, volume 3235 of Lecture Notes in Computer Science, 359–376. Springer, 2004.

Full Text:
Download PDF
Publisher Link:


We propose a framework for intrusion detection that is based on runtime monitoring of temporal logic specifications. We specify intrusion patterns as formulas in an expressively rich and efficiently monitorable logic called Eagle. Eagle supports data-values and parameterized recursive equations, and allows us to succinctly express security attacks with complex temporal event patterns, as well as attacks whose signatures are inherently statistical in nature. We use an online monitoring algorithm that matches specifications of the absence of an attack, with system execution traces, and raises an alarm whenever the specification is violated. We present our implementation of this approach in a prototype tool, called Monid and report our results obtained by applying it to detect a variety of security attacks in log-files provided by DARPA.

Keywords  Intrusion detection - security - temporal logic - runtime monitoring


    author = "Naldurg, Prasad and Sen, Koushik and Thati, Prasanna",
    editor = "de Frutos-Escrig, David and Núñez, Manuel",
    title = "A Temporal Logic Based Framework for Intrusion Detection",
    booktitle = "FORTE",
    crossref = "conf/forte/2004",
    ee = "",
    keywords = "formal methods, software engineering",
    pages = "359-376",
    year = "2004",

    editor = "de Frutos-Escrig, David and Núñez, Manuel",
    title = "Formal Techniques for Networked and Distributed Systems -
             FORTE 2004, 24th IFIP WG 6.1 International Conference, Madrid
             Spain, September 27-30, 2004, Proceedings",
    isbn = "3-540-23252-4",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "3235",
    year = "2004",