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

doi:10.3778/j.issn.1002-8331.1606-0076

计算机工程与应用 ›› 2017, Vol. 53 ›› Issue (1): 34-38.DOI: 10.3778/j.issn.1002-8331.1606-0076

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

秦嫚蔓，王峥，王莉

太原理工大学计算机科学与技术学院，太原 030024

出版日期:2017-01-01 发布日期:2017-01-10

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

QIN Manman, WANG Zheng, WANG Li

School of Computer Science and Technology, Taiyuan University of Technology, Taiyuan 030024, China

Online:2017-01-01 Published:2017-01-10

摘要/Abstract

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

关键词: 移动支付, 远程证明协议, 用户属性, 形式化分析, 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 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的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.

QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN[J]. Computer Engineering and Applications, 2017, 53(1): 34-38.

[1]	杨文霞，王峥，李娜，马建芬. 轻量级移动支付协议LMPP的安全性分析与改进[J]. 计算机工程与应用, 2019, 55(16): 88-93.
[2]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[3]	马远佳1，刘道微2. 一种改进的满足后向安全的RFID双向认证协议[J]. 计算机工程与应用, 2017, 53(9): 136-140.
[4]	余磊1，魏仕民1，卓泽朋2. 认证测试中协议主体串参数一致性研究[J]. 计算机工程与应用, 2015, 51(13): 86-91.
[5]	张璇1，2，林逸风1，白川1，王旭3，马暮婷1，于倩1，2. 基于贝叶斯网络的移动支付风险评估模型[J]. 计算机工程与应用, 2014, 50(5): 60-64.
[6]	余磊，魏仕民. 协议主体密钥在测试组件构造上的性质分析[J]. 计算机工程与应用, 2013, 49(6): 114-117.
[7]	刘永磊1，2，金志刚3. 无线局域网WPS安全性分析[J]. 计算机工程与应用, 2013, 49(21): 87-89.
[8]	范玉涛1，苏桂平2. 一种适于带时间戳安全协议的形式化分析方法[J]. 计算机工程与应用, 2012, 48(36): 116-120.
[9]	李沛武1，雷金娥2. 有色Petri网的扩展使用控制策略模型设计[J]. 计算机工程与应用, 2012, 48(33): 96-100.
[10]	李廷元1，2，秦志光1，刘晓东2，张选芳2. Needham-Schroeder 协议的认证测试方法形式化分析[J]. 计算机工程与应用, 2010, 46(19): 100-102.
[11]	周佳骏^１，马瑞兴^２，王峰³，李肖坚^3，4. 蠕虫智能扩散形式化分析及权策略算法实现[J]. 计算机工程与应用, 2010, 46(13): 90-94.
[12]	^{孔娟，曹利培} . TLS协议认证测试模型与形式化分析 [J]. 计算机工程与应用, 2009, 45(23): 100-103.
[13]	张　超,韩继红,王亚弟,朱玉娜. 改进的安全协议一阶逻辑模型[J]. 计算机工程与应用, 2008, 44(26): 95-98.
[14]	赵辉，李明楚，王智慧. 一种基于虚拟组织的网格安全协议形式化验证方法[J]. 计算机工程与应用, 2007, 43(24): 117-122.
[15]	范伟寇卫东李华平党岚君樊凯. 一种公平的移动支付协议[J]. 计算机工程与应用, 2007, 43(11): 201-203.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics