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

34 2017 ，53（1） Computer Engineering and Applications 计算机工程与应用 基于SPIN 的远程证明协议的形式化分析及改进 秦嫚蔓，王 峥，王 莉 QIN Manman, WANG Zheng, WANG Li 太原理工大学 计算机科学与技术学院，太原 030024 School of Computer Science and Technology, Taiyuan University of Technology, Taiyuan 030024, China QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN. Computer Engineering and Applications, 2017, 53 （1）：34-38. 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. Key words: mobile payment; remote attestation protocol; user attributes; formal analysis; SPIN model checking 摘 要：远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析，发现用户平 台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点，使用SPIN 模型检测工具，应用模型检测方 法对协议进行了形式化分析，检测出破坏性攻击漏洞。针对协议中的漏洞对协议进行改进，提出了一种基于用户属 性加盐哈希的方法，通过用户属性保证协议的安全传输。最后使用SPIN 检测改进后的协议，证明了改进方案的有 效性、安全性，阻断了发现的攻击。 关键词：移动支付；远程证明协议；用户属性；形式化分析；SPIN模型检测 文献标志码：A 中图分类号：TP309 doi ：10.3778/j.issn. 1002-8331.1606-0076 1 引言 机密信息和数据的泄露以及攻击者的破坏性攻击。因 现今移动互联快速发展，随着电子商务的盛行和移 此远程证明协议在移动支付的安全操作上有很重要的 [2] 动终端的普及，移动支付作为移动网络的一项服务能够