计算机工程与应用2017，Vol.53Issue(1)：34-38,72,6.DOI:10.3778/j.issn.1002-8331.1606-0076
基于SPIN的远程证明协议的形式化分析及改进
Formal analysis and improvement of remote attestation protocol based on the SPIN
摘要
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 attri-butes to ensure the safe transmission of the protocol. Finally, it uses the SPIN to test the improved protocol, proves the va-lidity and security of the improved protocol, and blocks the attacks.关键词
移动支付/远程证明协议/用户属性/形式化分析/SPIN模型检测Key words
mobile payment/remote attestation protocol/user attributes/formal analysis/SPIN model checking分类
信息技术与安全科学引用本文复制引用
秦嫚蔓,王峥,王莉..基于SPIN的远程证明协议的形式化分析及改进[J].计算机工程与应用,2017,53(1):34-38,72,6.基金项目
国家高技术研究发展计划（863）项目（No.2014AA015204）。 （）
