提出一种基于行为时序逻辑的入侵取证的形式化方法，其描述语言能够准确描述入侵证据、系统知识以及攻击行为，并具有在部分数据缺失的情况下进行非确定性推理的能力；其自动验证工具能够寻求额外的证据并可检查是否有可能的攻击与这些证据相符。实例研究表明，这种方法不依赖于具体的攻击技术和操作系统，不惧证据的缺失，能够有效搜寻更多的证据并重建可能的攻击场景。