动态远程证明协议及其形式化分析

摘要：

针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态.针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻规则等新的推理规则,利用扩展的LS2逻辑对DRAP协议进行分析,分析表明DRAP中可重置配置寄存器中的扩展序列能够反映平台中程序的实时运行状态,并且在TPM可信和证明代理可信的前提下,远程验证者能够有效验证平台的实时可信状态.

关键词：动态度量、远程证明、时间戳、LS2逻辑、形式化分析

所属期刊栏目：33

分类号：TP309(计算技术、计算机技术)

资助基金：国家973重点基础研究发展计划基金项目2007CB311100;国家863高技术研究发展计划基金项目2009AA01Z437;国家核高基项目2010ZX01037-001-001;信息安全国家重点实验室中国科学院软件研究所开放课题

在线出版日期：2012-11-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：2901-2905