%0 Journal Article
%T 满足对应性属性的平台配置证明
%A 张帆
%A 高杨
%A 高雪原
%J 计算机应用
%D 2018
%R 10.11772/j.issn.1001-9081.2017082168
%X 摘要 针对完整性报告协议（IRP）存在局部和全局攻击的安全隐患，对StatVerif进行语法扩展，增加了与完整性度量相关的构造算子和析构算子，通过对平台配置证明（PCA）安全进行分析，发现其存在的局部攻击和全局攻击，包括通过未授权命令对平台配置寄存器和存储度量日志进行篡改。对攻击者能力进行了建模，详细说明了攻击者如何通过构造子和析构子形成知识，进而对平台配置证明进行攻击。最后，在平台配置证明不满足对应性属性的情况下，从理论上证明了攻击序列的存在，并给出了平台配置证明满足局部可靠和全局可靠的条件，通过形式化验证工具Proverif证明了命题的合理性
%K 可信计算
%K 完整性报告协议
%K 平台配置证明
%K 对应性属性
%K StatVerif演算
%K Proverif验证
%U http://www.joca.cn/CN/abstract/abstract21520.shtml