Research in computer and network forensic investigation has recently addressed the development of procedural guidelines, technical documents, and semi-automation tools. It has however omitted the need of formal proof. This work provides a novel approach that formalizes and automates the proof in digital forensic investigation. First, it brings out a formal logic-based language, called S-TLA+, to enable reasoning on systems with uncertainty, by adding forward hypotheses to fulfill potential lack of details. S-TLA+ is suitable for the description of evidences, as well as elementary scenarios fragments representing the investigators knowledge. Secondly, the proposal provides an automated verification tool, S-TLC, to prove the correctness of S-TLA+ specifications. It checks whether there are possible hacking scenarios that meet the available digital evidences, and explores additional evidences. To demonstrate its effectiveness, the formalized analysis is applied on a compromised host. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Rekhis, S., & Boudriga, N. (2005). A temporal logic-based model for forensic investigation in networked system security. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3685 LNCS, pp. 325–338). https://doi.org/10.1007/11560326_25
Mendeley helps you to discover research relevant for your work.