A Temporal Logic-Based Model for Forensic Investigation in Networked System Security - Computer Network Security - page 337

(0 , , “”) { (“ weakpwd ” , ∇ ) }

LogAsUsr
(1 , “ usr ” , “ logon ” , “”) { (“ weakpwd ” , ∇ ) }

Instsoft

(1 , “ usr ” , “ logon ” , “ exploit ”) { (“ weakpwd ” , ∇ ) }

OffBrForce

ExpLclVuln

(2 , “ usr ” , “ logon ” “ root ” , “ logon ” , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

CleanLog

(2 , “ usr ” , “ logon ” “ root ” , “ logoff ” , “”) { (“ weakpwd ” , “ pwdhashcomp ”) }

(2 , , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

CleanLog

DelSoft

, “”) (“ weakpwd ” , “ pwdhashcomp ”)
(“ weakpwd ” , “ vulbin ”)

Exit

(2 ,

(2 , “ root ” , “ logoff ” , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

Exit

, “”) (“ weakpwd ” , “ pwdhashcomp ”)
(“ weakpwd ” , “ vulbin ”)

(2 , “ root ” , “ logoff ”

Fig. 4. Scenarios generated in forward chaining phase

(0 , , “ audittool ”) { (“ weakpwd ” , ∇ ) }

LogAsUsr

(1 , “ usr ” , “ logon ” , “ audittool ”) { (“ weakpwd ” , ∇ ) }

ExtSoft

(1 , “ usr ” , “ logon ” , “ exploit ”) { (“ weakpwd ” , ∇ ) }

ExpLclVuln

(2 , “ usr ” , “ logon ” “ root ” , “ logon ” , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

CleanLog

(2 , , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

DelSoft

(2 , , “”) (“ weakpwd ” , “ pwdhashcomp ”)
(“ weakpwd ” , “ vulbin ”)

Exit

(2 , “ root ” , “ logoff ” , “ exploit ”) { (“ weakpwd ” , “ vulbin ”) }

Exit

(2 , “ root ” , “ logoff ” , “”) (“ weakpwd ” , “ pwdhashcomp ”)
(“ weakpwd ” , “ vulbin ”)

Fig. 5. Scenarios generated in backward chaining phase

succeeds in escalating its privilege by performing an oine brute-force of
the root password. It cleans its logged activity and logs off from the system.
Fortunately, the latter activity is logged.
2. An intruder guesses a weak user password and logs in to the system, gaining
an unprivileged access. After that, it installs a malicious tool and exploits
a vulnerability in one of the installed super-user commands, obtaining thus
a privileged access. Before cleaning the log file and leaving the system, the
intruder either deletes its installed tool or leaves such kind of evidence.

The generated scenario prevents inconsistency from occurring. In fact, action
ChangeID does not belong to the scenario since it contains a hypothesis that is
inconsistent with the one occurring in LogAsUsr according to the definition of
predicate Inconsistency . The graph of Figure 5 is the graph generated after the
execution of forward and backward chaining phases. For readability reasons, it