基于协议验证的时间自动机取证模型

摘要

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