Abstract: Remote attestation is one of the effective methods to solve the problem of mobile payment security. To analyze remote 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 formal analysis to the protocol by using the model checking method, and detects the destructive attack vulnerability.To improve the protocol for these holes, the paper puts forward a method based on user attributes to add salt to Hash, using user attributes to ensure the safe transmission of the protocol. Finally, it uses the SPIN to test the improved protocol, proves the validity and security of the improved protocol, and blocks the attacks.

Key words: mobile payment, remote attestation protocol, user attributes, formal analysis, SPIN model checking

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

关键词: 移动支付, 远程证明协议, 用户属性, 形式化分析, SPIN模型检测