满足对应性属性的平台配置证明
来源：计算机应用杂志2018年第2期北京时间：
作者：徐明迪, 高杨, 高雪原, 张帆
单位：1. 武汉数字工程研究所, 武汉 430205;2. 武汉轻工大学 数学与计算机学院, 武汉 430023
摘要：针对完整性报告协议（IRP）存在局部和全局攻击的安全隐患，对StatVerif进行语法扩展，增加了与完整性度量相关的构造算子和析构算子，通过对平台配置证明（PCA）安全进行分析，发现其存在的局部攻击和全局攻击，包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模，详细说明了攻击者如何通过构造子和析构子形成知识，进而对平台配置证明进行攻击。最后，在平台配置证明不满足对应性属性的情况下，从理论上证明了攻击序列的存在，并给出了平台配置证明满足局部可靠和全局可靠的条件，通过形式化验证工具Proverif证明了命题的合理性。
关键词：可信计算,完整性报告协议,平台配置证明,对应性属性,StatVerif演算,Proverif验证
基金资助：国家自然科学基金资助项目（61502438）。
