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

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

作　　者：秦嫚蔓 王峥[1] 王莉[1] QIN Manman;WANG Zheng;WANG Li(School of Computer Science and Technology, Taiyuan University of Technology, Taiyuan 030024, China)

机构地区：[1]太原理工大学计算机科学与技术学院,太原030024

出　　处：《计算机工程与应用》2017年第1期34-38,72,共6页Computer Engineering and Applications

基　　金：国家高技术研究发展计划(863)项目(No.2014AA015204)

摘　　要：远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用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.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]