远程证明安全协议的设计与验证

Design and validation for a remote attestation security protocol

通过对现有远程证明协议交互协议的分析,提出了一种改进的远程证明协议。为了验证该协议是否符合安全需求,采用安全协议形式化分析方法中的基于攻击类的CSP方法对协议进行了CSP建模,同时通过对模型进行的FDR检测,发现了协议中存在的漏洞,给出了漏洞的修改方案。经过再次验证得到了符合安全需求的安全协议。该协议可用于可信计算的远程证明,能够保证远程证明的正确完成和交互过程中消息的保密性、完整性、认证性及新鲜性。

By analyzing current remote attestation model, an improved remote attestation model was provided and de-signed.In order to verify whether it conforms to security requirement, a formal analysis method CSP was used to analyze the protocol and model it with CSP method.Meanwhile, it was checked with FDR tool.A loophole of the protocol was found.For solving the problem, an improvement to the protocol was made.It has been verified that security properties can be guaranteed by the re-validate.This protocol can be used for the remote attestation in trust computing and it can ensure the secrecy, integrity, authentication and freshmen in the interoperation process of the protocol.