City Research Online

Abstract

Digital forensic investigations can be disrupted when actors tamper with digital artefacts on devices before they are seized. This activity, when undetected, misleads investigations and results in incorrect findings. Several established research approaches in digital forensics use formal models to identify whether a specific action has occurred through event reconstruction. However, we address two specific concerns which limit their use when investigating tampering actions. First, current understanding of tampering is based solely on informal natural language descriptions; no representations of tampering exist that can be used with the reasoning applied with formal models. Second, mathematically solving these types of reconstruction problems relies on generating relevant input models and analysing their state-space, which is considered to be impractical for real-life cases. For the first of these concerns, we extend the ‘Temporal Logic of Security Actions’ (S-TLA) language to describe a general system and introduce the property of ‘action visibility’. We use this to create a model that represents one type of tampering, artefact destruction, and characterise it into four specific sub-types. For the second concern, we apply inductive reasoning to study the impact of artefact destruction on a generic system through comparing its state before and after the action. From this we characterise features of a system which has been subject to this tampering action. We present two brief case studies which illustrate how such features can be used to recognise whether tampering has occurred. Finally, we extend this technique to other types of artefact tampering to create a knowledge framework that can be used to aid the recognition of tampering activity.

Publication Type:	Article
Additional Information:	© 2026 The Authors. Published by Elsevier Ltd. This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Publisher Keywords:	Tampering, Anti-forensics, Digital artefacts, Modelling, Temporal logic
Subjects:	Q Science > QA Mathematics T Technology > T Technology (General)
Departments:	School of Science & Technology
SWORD Depositor:	Symplectic Administrator

Export

Downloads