A Formal Approach for the Reconstruction of Potential Attack Scenarios

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 evidences. 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.