Logic-based approach for digital forensic investigation in communication Networks

In this paper, we provide a logic for digital investigation of security incidents and its high-level-specification language. The logic is used to prove the existence or non-existence of potential attack scenarios which, if executed on the investigated system, would produce the different forms of specified evidence. To generate executable attack scenarios showing with details how the attack scenario was conducted and how the system behaved accordingly, we develop in this paper a Model Checker tool which provides tolerance to unknown attacks and integrates a technique for hypothetical actions generation