Abstract: Concerning the security problem of local and global attacks on the Integrity Report Protocol (IRP), the StatVerif syntax was extended by adding constructors and destructors associated with the integrity measurement. The security of the Platform Configuration Attestation (PCA) was analyzed and the local and global attacks were found, including tampering the platform configuration register or revising stored measurement log by running unauthorized commands. The abilities of attackers were modeled, and how attackers accumulated knowledge and tampered PCA protocol by using constructors and destructors was introduced. Finally, the existence of attacking sequence was proved theoretically when PCA does not satisfy the correspondence property; and several propositions that PCA can meet the local reliability and gloabal reliability were given, which were proved by the formal verification tool Proverif.

Key words: trusted computing, Integrity Report Protocol (IRP), Platform Configuration Attestation (PCA), correspondence property, StatVerif calculus, Proverif verification

摘要： 针对完整性报告协议（IRP）存在局部和全局攻击的安全隐患，对StatVerif进行语法扩展，增加了与完整性度量相关的构造算子和析构算子，通过对平台配置证明（PCA）安全进行分析，发现其存在的局部攻击和全局攻击，包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模，详细说明了攻击者如何通过构造子和析构子形成知识，进而对平台配置证明进行攻击。最后，在平台配置证明不满足对应性属性的情况下，从理论上证明了攻击序列的存在，并给出了平台配置证明满足局部可靠和全局可靠的条件，通过形式化验证工具Proverif证明了命题的合理性。

关键词: 可信计算, 完整性报告协议, 平台配置证明, 对应性属性, StatVerif演算, Proverif验证