Computer intrusion forensic based on temporal logic of actions
Li Xiang · Jisuanji yingyong yanjiu · 2011
This paper put forward a formalist based on temporal logic of actions.Its specifying language could be used to descript explicitly information about evidences and system knowledge and attack technologies.Its formal verification tool could generate automatically additional evidence and determined the potential attack scenarios that met the available evidences.Case study shows that this method doesn't depend on special attack technologies and operating systems,it can tolerate the missing of evidence and select additional evidence effectively and reconstruct attack scenarios.