基于SPIN的远程证明协议的形式化分析及改进

Formal analysis and improvement of remote attestation protocol based on the SPIN

远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检测出破坏性攻击漏洞。针对协议中的漏洞对协议进行改进,提出了一种基于用户属性加盐哈希的方法,通过用户属性保证协议的安全传输。最后使用SPIN检测改进后的协议,证明了改进方案的有效性、安全性,阻断了发现的攻击。

Remote attestation is one of the effective methods to solve the problem of mobile payment security. To analyzeremote attestation protocol based on trusted computing, it finds that the user platform configuration information privacy,user authentication and certification of remote verifier have vulnerabilities, SPIN model checking tool is applied formalanalysis to the protocol by using the model checking method, and detects the destructive attack vulnerability.To improvethe protocol for these holes, the paper puts forward a method based on user attributes to add salt to Hash, using user attributesto ensure the safe transmission of the protocol. Finally, it uses the SPIN to test the improved protocol, proves the validityand security of the improved protocol, and blocks the attacks.