基于SPIN的远程证明协议的形式化分析及改进
来源：计算机工程与应用杂志2017年第1期北京时间：
作者：秦嫚蔓，王 峥，王 莉
单位：太原理工大学 计算机科学与技术学院，太原 030024
摘要：远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析，发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点，使用SPIN模型检测工具，应用模型检测方法对协议进行了形式化分析，检测出破坏性攻击漏洞。针对协议中的漏洞对协议进行改进，提出了一种基于用户属性加盐哈希的方法，通过用户属性保证协议的安全传输。最后使用SPIN检测改进后的协议，证明了改进方案的有效性、安全性，阻断了发现的攻击。
关键词：移动支付,远程证明协议,用户属性,形式化分析,SPIN模型检测
