基于行为时序逻辑的多方协作取证研究

李均涛++唐郑熠++张金磊

【 摘 要 】 论文提出了一种基于行为时序逻辑和片面性理论的多方协作取证的形式化方法，有望在多方参与的调查取证中验证不可观察的行为证据，并将其应用到一个取证实例中。

【 关键词 】 入侵取证；行为时序逻辑；片面性；多方协作取证

【 中图分类号 】 TP309.2

【 文献标识码 】 A

Multilateral Cooperation Intrusion Forensics Based onTemporal Logic of Actions

LI Jun-tao 1 Tang Zheng-yi 2 Zhang Jin-lei 1

（1.Information School of Guizhou University of Finance and Ecnomics GuizhouGuiyang 550025；

2.College of Information Science and Engineering， Fujian University of Technology FujianFuzhou 350118）

【 Abstract 】 Put foreword a formalist method of multi-party cooperation intrusion forensics based on Temporal Logic of Actions and Opacity Theory， expected to verify the evidence not easy observed， and apply it to an intrusion forensic instance.

【 Keywords 】 computer intrusion forensic； temporal logic of actions； opacity； multilateral cooperation intrusion forensics

1 引言

在取证调查时，调查者的主要难题就是证明入侵者行为是否蓄意而为，这可以用系统状态的性质来刻画，即这些状态是否是入侵者的伪装，这使得对它们的计算更加难以执行。对入侵者来说，调查者作为第三方仅有有限的关于它们攻击行为的观测记录，即所能收集到的不完备的证据集。举例来说，一个入侵检测系统的报警文件仅仅给出了有关远程执行命令集的信息，并不能向展示系统是如何被攻击的。从这一考虑出发，有必要对文献[1]提出的形式化方法进行补充，使之能够证明源于入侵活动不完全观测的数字证据。

2 多方协作取证的理论基础

不同的观察者从不同的角度观察同一个事务往往会得出不同的观察结果，瞎子摸象的故事就是这种现象的一个典型代表。对安全事件的取证调查也会碰到这样的情况，即不同的调查者依据各自的知识和技术，对收集到的不同证据集进行分析，这必然会产生相互间的合作问题。而这种协作也必然会给取证调查工作带来新的性质。

为了更好地处理多方协作取证，提出了一种片面性理论。……