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

shows only the new generated scenarios compared to the ones of Figure 4. Mainly,
a new scenario is added. It strongly resembles to the second one generated in
forward chaining phase, except that the system is initially housing a security
auditing software and the hacker is using one of the commands that come with
such software as an exploit tool, instead of installing its own one.
7Con lu on
We proposed in this paper a novel formal logic-based language entitled S-TLA +
to achieve a tremendous aspect in digital forensic investigation: the reconstruc-
tion of potential hacking scenarios and the providing of new evidences that could
complement the available ones. S-TLA + uses a formalism that allows handling
hypotheses whenever there is a lack of details to demonstrate some part of an
attack scenario. We have also described S-TLC as a new automated formal verifi-
cation tool that is able to handle S-TLA + specifications. Its main advantage lies
in its robustness in managing hypotheses and representing states. Considering
implementing and testing this tool represents a continuation of this work.
References
1. Kruse, W.G., Heiser, J.G.: Computer Forensics: Incident Response Essentials.
Pearson Education (2001)
2. Stephenson, P.: Modeling of post-incident root cause analysis. International Journal
of Digital Evidence, Vol. 2, No. 2 (2003)
3. Elsaesser, C., Tanner, M.C.: Automated diagnosis for computer forensics. tech.
rep., The MITRE Corporation (2001)
4. Stallard, T., Levitt, K.: Automated analysis for digital forensic science: Semantic
integrity checking. Proceedings of the 19th Annual Computer Security Applications
Conference (2003)
5. Rekhis, S., Boudriga, N.: A Formal Logic-based Language and an Automated Ver-
ification Tool For Computer Forensic Investigation. Proceedings of the 20th ACM
Symposium on Applied Computing (SAC 2005) (2005)
6. Lamport, L.: Specifying Systems: The TLA + Language and Tools for Hardware
and Software Engineers. Addison-Wesley (2002)
7. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA + specifications. Conference
on Correct Hardware Design and Verification Methods (1999) 54-66
8. Keppens, J., Zeleznikow, J.: A model based reasoning approach for generating
plausible crime scenarios from evidence. Proceedings of the 9th International Con-
ference on Artificial Intelligence and Law (2003)
9. Lamport, L.: The temporal logic of actions. ACM Transactions on Programming
Languages and Systems, Vol. 16 (1994) 872-923
10. de Kleer, J.: An assumption-based TMS. Artificial Intelligence, Vol. 28, No. 2
(1986) 127-162