A formal model for event reconstruction in digital forensic investigation

Event reconstruction is an important phase in digital forensic investigation, which determines what happened during the incident. The digital investigator uses the findings of this phase to prepare reports for the court. Since the results must be reproducible and verifiable, it is necessary that the event reconstruction methods be rigorous and strict. In order to fulfill the legal requirements, this study proposes an event reconstruction framework which is based on the formal mathematical methods. In particular, it uses the temporal logic model checking that is an automatic verification technique. The idea is that the system under investigation is modeled as a transition system. Then the digital forensic property is specified using the modal μ-calculus. Finally, a model checking algorithm verifies whether the transition system meets the property. In order to demonstrate the proposed formal event reconstruction framework, an abstract model of the FAT file system is presented and some digital forensic properties are formulated. A big problem in model checking is the so-called state space explosion. This study addresses this problem and suggests some solutions to it. Finally, the proposed framework is applied to a case study to demonstrate how some hypotheses can be proved or refuted.