伴随着计算机技术的快速发展，涉及到计算机犯罪的案件频繁发生，计算机取证技术应运而生。计算机取证具有自身的特点，要求在取证过程中，尽最大可能地搜集到所有涉案电子证据、保证电子数据的原始性、确保电子数据取证结果可信。如何保证提供的证据能够呈堂并作为庭审的依据，是一个亟待解决的难题。纵观计算机取证近些年的研究现状，技术研究的重点放在电子数据的获取上，忽视了数据分析和取证理论的研究。鉴于此，本文在已有研究的基础上，提出了计算机取证中电子数据的静态属性语义特征模型和计算机取证过程中动态行为形式化模型，从而保证取证过程电子数据的原始性、完整性、一致性和可信性以及取证方法的规范化。在查阅大量的文献后，本文做的主要工作如下：1）总结已有研究成果，研究分析电子数据可信取证的理论基础，为可信取证形式化模型提供基本的理论支撑。2）在已有的电子数据可信取证体系的理论基础上，分析现有计算机取证方法的不足，并由此提出计算机取证中电子数据的静态属性语义特征模型和计算机取证过程中动态行为形式化模型。3）使用FODA和OCL形式化描述计算机取证的电子数据的静态属性语义特征模型。4）将层次时间自动机和基于瀑布模型的可信取证方法结合，形式化描述了计算机取证过程中动态行为形式化模型。5）针对电子数据的静态属性语义特征模型给出实例分析；针对计算机取证过程中动态行为形式化模型使用UPPAAL仿真和验证。