论文部分内容阅读
如何确保计算机获取的证据真实可靠,成为法院上可供参考的法律依据,这是一个迫切需要解决的问题。因此,需要一种形式化描述方法使得数字取证调查具有可靠性和可信性。文中提出一种基于协议验证的TA（时间自动机）形式化描述方法,利用取证工具获得具有时间属性的行为数据,并用TA描述计算机取证的动态事件重构行为,通过UPPAAL工具进行需求分析和验证来达到取证的目的。