A formal model for event reconstruction in digital forensic investigation |
| |
Affiliation: | 1. School of Technology and Management - Polytechnic Institute of Leiria, Leiria, Portugal;2. Instituto de Telecomunicações, Portugal;3. Computer Science and Communication Research Centre, Portugal;1. CheckSem Team, Laboratoire Le2i, UMR CNRS 6306, Faculté des Sciences Mirande, Université de Bourgogne, BP47870, 21078 Dijon, France;2. School of Computer Science & Informatics, University College Dublin, Belfield, Dublin 4, Ireland;1. School of Computer Engineering and Physical Sciences, University of Central Lancashire, Preston, UK;2. General Department of Forensic Sciences and Criminology, Dubai Police G.H.Q., Dubai, United Arab Emirates;3. School of Psychology, University of Central Lancashire, Preston, UK;4. College of Engineering and Technology, University of Derby, Derby, UK;5. College of Technological Innovation, Zayed University, Dubai, United Arab Emirates |
| |
Abstract: | 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. |
| |
Keywords: | Formal event reconstruction Formal digital investigation Formal mathematical methods Model checking Process algebra Modal μ-calculus State space explosion |
本文献已被 ScienceDirect 等数据库收录! |
|