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

Dynamic remote attestation protocol and it's formal analysis

作　　者：辛思远[1,2] 赵勇[3,2] 王婷 

机构地区：[1]解放军信息工程大学电子技术学院,河南郑州450004 [2]中国科学院软件研究所信息安全国家重点实验室,北京100049 [3]北京工业大学计算机学院,北京100124 [4]65047部队,辽宁沈阳110000

出　　处：《计算机工程与设计》2012年第8期2901-2905,共5页Computer Engineering and Design

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

摘　　要：针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态。针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻规则等新的推理规则,利用扩展的LS2逻辑对DRAP协议进行分析,分析表明DRAP中可重置配置寄存器中的扩展序列能够反映平台中程序的实时运行状态,并且在TPM可信和证明代理可信的前提下,远程验证者能够有效验证平台的实时可信状态。Aimed at the process runtime attack threat of remote attestation, a dynamic remote attestation protocol （DRAP） is designed, the process runnig in the memory is measured in real time and the dynamic running state of the platform is reported to remote verifier. Based on the TPM function usred in DRAP, the LS2 logic is extended, and the PCR reset rule and time rule is imported into LS2. Finally, the security and effectiveness properties of DRAP are formally analysed by LS2. It＇s analysed that the extended sequence of reset PCR in DRAP can reflect the platform＇s process real time running state, and in the premise of trusted TPM and trusted attestation agent, verifier can effectively verify the real time trusted state of remote platform.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]