A formal logic-based language and an automated verification tool for computer forensic investigation

ABSTRACT

In this paper, a formal logic-based language, called S-TLA⁺, is proposed for computer forensic investigation. It allows an unambiguous description of evidences, a modeling of the forensic expert knowledge in the form of hacking scenarios fragments, and a reasoning capability with uncertainty by filling in potential lack of data with hypotheses. The proposal is complemented by an automated formal verification tool, called S-TLC which helps exploring additional evidences and checks whether there are plausible hacking scenarios that meet the available evidences.

REFERENCES

• 1: Johan de Kleer, An assumption-based TMS, Artificial Intelligence, v.28 n.2, p.127-162, March 1986 [doi>10.1016/0004-3702(86)90080-9]
• 2: Elsaesse, C., and Tanner, M. C. Automated diagnosis for computer forensics. Tech. rep., The MITRE Corporation, 2001.
• 3: Jeroen Keppens , John Zeleznikow, A model based reasoning approach for generating plausible crime scenarios from evidence, Proceedings of the 9th international conference on Artificial intelligence and law, June 24-28, 2003, Scotland, United Kingdom [doi>10.1145/1047788.1047796]
• 4: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 5: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 6: Shanmugasundaram, K., and Memon, N. Automatic reassembly of document fragments via data compression. In Proceeding of the Digital Forensics Research Workshop (2002).
• 7: Tye Stallard , Karl Levitt, Automated Analysis for Digital Forensic Science: Semantic Integrity Checking, Proceedings of the 19th Annual Computer Security Applications Conference, p.160, December 08-12, 2003

INDEX TERMS

Keywords:
S-TLA⁺, S-TLC, formal forensic investigation, temporal logic of security actions