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

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