基于Tamarin的门罗币支付协议分析方法

doi:10.3969/j.issn.1671-1122.2024.05.009

信息网络安全 ›› 2024, Vol. 24 ›› Issue (5): 756-766.doi: 10.3969/j.issn.1671-1122.2024.05.009

基于Tamarin的门罗币支付协议分析方法

李雨昕, 黄文超(), 王炯涵, 熊焰

中国科学技术大学计算机科学与技术学院，合肥 230026

收稿日期:2023-12-21 出版日期:2024-05-10 发布日期:2024-06-24
通讯作者: 黄文超 E-mail:huangwc@ustc.edu.cn
作者简介:李雨昕（2000—），女，安徽，硕士研究生，主要研究方向为区块链和网络协议分析|黄文超（1982—），男，湖北，副教授，博士，CCF会员，主要研究方向为网络安全、漏洞挖掘和形式化建模|王炯涵（2000—），男，甘肃，硕士研究生，主要研究方向为区块链和网络协议分析|熊焰（1960—），男，安徽，教授，博士，CCF会员，主要研究方向为网络安全、漏洞挖掘和形式化建模
基金资助:
国家自然科学基金(62372422);国家自然科学基金(61972369);国家自然科学基金(62102385);安徽省自然科学基金(2108085QF262);中央高校基本科研业务费专项资金(WK2150110024)

Analysis Method of Monero Payment Protocol Based on Tamarin

LI Yuxin, HUANG Wenchao(), WANG Jionghan, XIONG Yan

School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China

Received:2023-12-21 Online:2024-05-10 Published:2024-06-24
Contact: HUANG Wenchao E-mail:huangwc@ustc.edu.cn

摘要/Abstract

摘要：

门罗币作为一款基于区块链技术的高度匿名加密货币协议，旨在为用户提供强大的隐私保护功能。与其他加密货币不同，门罗币通过独特的支付协议对用户的交易隐私加强保护。然而，支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析或拦截，从而威胁用户的隐私安全。目前，对门罗币支付协议的研究主要集中在对匿名性漏洞的攻击，大部分攻击从外部特征出发，缺少对门罗币机制进行探索，不能充分保障支付过程的安全性和不可追踪性。因此需要进行更系统化的分析，以全面评估门罗币支付协议的安全性和不可追踪性。文章从模型规则、属性定义等角度对门罗币支付协议进行细粒度建模，并运用已有的Tamarin工具对相关属性进行验证，研究结果揭示了多个门罗币支付协议漏洞，并给出优化建议。

关键词: 门罗币, Tamarin, 支付协议, 符号模型

Abstract:

Monero, as a highly anonymous cryptocurrency protocol based on blockchain technology, aims to provide robust privacy protection for users. Unlike other cryptocurrencies, Monroe coin enhances user transaction privacy protection through its unique payment protocol. However, security vulnerabilities within the payment protocol may lead attackers to analyze or intercept transaction information, thereby posing a threat to user privacy. Currently, research on the Monero payment protocol primarily focuses on attacks targeting anonymity vulnerabilities, often starting from external features and lacks exploration of the intrinsic mechanisms of Monero itself, which insufficiently ensuring the security and untraceability of the payment process. Therefore, a more systematic analysis is needed to comprehensively evaluate the security and untraceability of the Monero payment protocol. This paper provided a detailed modeling of the Monero payment protocol from various perspectives, including model rules and attribute definitions. The study utilized the existing Tamarin tool to verify relevant properties. The research findings reveal multiple vulnerabilities in the Monero payment protocol and offer optimization recommendations.

Key words: Monero, Tamarin, payment protocol, symbolic model

中图分类号:

TP309

李雨昕, 黄文超, 王炯涵, 熊焰. 基于Tamarin的门罗币支付协议分析方法[J]. 信息网络安全, 2024, 24(5): 756-766.

LI Yuxin, HUANG Wenchao, WANG Jionghan, XIONG Yan. Analysis Method of Monero Payment Protocol Based on Tamarin[J]. Netinfo Security, 2024, 24(5): 756-766.

图/表 6

图1

图2

表1

表2

图3

图4

参考文献 22

[1]	KUMAR A, FISCHER C, TOPLE S, et al. A Traceability Analysis of Monero’s Blockchain[C]// Springer. 22nd European Symposium on Research in Computer Security. Heidelberg: Springer, 2017: 153-173.
[2]	MÖSER M, SOSKA K, HEILMAN E, et al. An Empirical Analysis of Traceability in the Monero Blockchain[EB/OL]. (2017-04-13)[2023-12-03]. https://arxiv.org/abs/1704.04299.
[3]	YU Zuoxia, AU M H, YU Jiangshan, et al. New Empirical Traceability Analysis of CryptoNote-Style Blockchains[C]// Springer. International Conference on Financial Cryptography and Data Security. Heidelberg: Springer, 2019: 133-149.
[4]	CHERVINSKI J O M, KREUTZ D, YU Jiangshan. FloodXMR: Low-Cost Transaction Flooding Attack with Monero’s Bulletproof Protocol[EB/OL]. (2019-05-10)[2023-12-03]. https://eprint.iacr.org/2019/455.
[5]	LIU Di, WANG Ziyi, LI Dawei, et al. Formal Analysis and Improvement Methods of 5G AKA Protocol Based on Tamarin[J]. Journal of Cryptologic Research, 2022, 9(2): 237-247.
	刘镝, 王梓屹, 李大伟, 等. 基于Tamarin的5G AKA协议形式化分析及其改进方法[J]. 密码学报, 2022, 9(2): 237-247.
[6]	ZHENG Hongbing, WANG Huanwei, ZHAO Qi, et al. Tamarin-Based Security Analysis of MQTT Protocol[J]. Application Research of Computers, 2023, 40(10): 3132-3137, 3143.
	郑红兵, 王焕伟, 赵琪, 等. 基于Tamarin的MQTT协议安全性分析方法[J]. 计算机应用研究, 2023, 40(10): 3132-3137, 3143.
[7]	BAO Xianglin, XIONG Yan, HUANG Wenchao, et al. Detection of the Computational Power Stealing Attack in Bitcoin Proto-Cols Based on Smart Verif[J]. Acta Electronica Sinica, 2021, 49(12): 2390-2398. doi: 10.12263/DZXB.20201194
	包象琳, 熊焰, 黄文超, 等. 基于Smart Verif的比特币底层协议算力盗取漏洞发现[J]. 电子学报, 2021, 49(12): 2390-2398. doi: 10.12263/DZXB.20201194
[8]	XIONG Yan, SU Cheng, HUANG Wenchao, et al. {SmartVerif}: Push the Limit of Automation Capability of Verifying Security Protocols by Dynamic Strategies[C]// USENIX. 29th USENIX Security Symposium (USENIX Security 20). Berkeley: USENIX, 2020: 253-270.
[9]	MACKENZIE A, NOETHER S, TEAM M C. Improving Obfuscation in the Cryptonote Protocol[EB/OL]. (2015-01-26)[2023-12-03]. https://www.semanticscholar.org/paper/MRL-0004-Improving-Obfuscation-in-the-CryptoNote-Mackenzie-Noether/5917a3dfa83f8aff6a10539da236b15fe06956da.
[10]	NOETHER S, MACKENZIE A. Ring Confidential Transactions[J]. Ledger, 2016(1): 1-18.
[11]	LIU J K, WEI V K, WONG D S. Linkable Spontaneous Anonymous Group Signature for Ad Hoc Groups[C]// Springer. 9th Australasian Conference (ACISP 2004). Heidelberg: Springer, 2004: 325-335.
[12]	LEE K, MILLER A. Authenticated Data Structures for Privacy-Preserving Monero Light Clients[C]// IEEE. 2018 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW). New York: IEEE, 2018: 20-28.
[13]	WIJAYA D A, LIU J, STEINFELD R, et al. Monero Ring Attack: Recreating Zero Mixin Transaction Effect[C]// IEEE. 2018 17th IEEE International Conference On Trust, Security and Privacy In Computing and Communications/12th IEEE International Conference On Big Data Science and Engineering (TrustCom/BigDataSE). New York: IEEE, 2018: 1196-1201.
[14]	WIJAYA D A, LIU J, STEINFELD R, et al. Anonymity Reduction Attacks to Monero[C]// Springer. 14th International Conference on Information Security and Cryptology. Heidelberg: Springer, 2019: 86-100.
[15]	LI Yannan, YANG Guomin, SUSILO W, et al. Traceable Monero: Anonymous Cryptocurrency with Enhanced Accountability[J]. IEEE Transactions on Dependable and Secure Computing, 2019, 18(2): 679-691.
[16]	CAO Tong, YU Jiangshan, DECOUCHANT J, et al. Exploring the Monero Peer-to-Peer Network[C]// Springer. 24th Financial Cryptography and Data Security. Heidelberg: Springer, 2020: 578-594.
[17]	DIFFIE W, HELLMAN M E. New Directions in Cryptography[J]. IEEE Transactions on Information Theory, 2022, 22(6): 365-390.
[18]	SILVERMAN J H. The Arithmetic of Elliptic Curves[M]. New York: Springer, 2009.
[19]	PEDERSEN T P. Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing[C]// Springer. 2001 Annual International Cryptology Conference. Heidelberg: Springer, 2001: 129-140.
[20]	MEIER S, SCHMIDT B, CREMERS C, et al. The TAMARIN Prover for the Symbolic Analysis of Security Protocols[C]// Springer. 25th International Conference on Computer Aided Verification (CAV 2013). Heidelberg: Springer, 2013: 696-701.
[21]	DOLEV D, YAO A. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208.
[22]	DREIER J, KASSEM A, LAFOURCADE P. Formal Analysis of E-Cash Protocols[C]// IEEE. 2015 12th International Joint Conference on E-Business and Telecommunications (ICETE). New York: IEEE, 2015(4): 65-75.

安全属性	代码	代码说明
交易一致性	lemma Menero_payment_Consensus: all-traces" All payment #i.(Blockin(payment)@#i) ==> not (Ex #j.(Pay_fail(payment)@#j))"	如果一笔交易在时间#i已经被门罗币网络上链，则不存在该交易在时间#j交易失败，即交易的发送方和接收方都能确认该交易。
抗双花性	lemma Menero_Menero_double_spend: all-traces" All T0 skA skB1 #i.(BlockIn(《<T0, pk(skB1)>, sign(skA,<T0, pk(skB1)>)>, pk(skA)>)@#i) ==> not (Ex skB2 #j.(BlockIn(《<T0, pk(skB2)>, sign(skA,<T0, pk(skB2)>)>, pk(skA)>)@#j) &(not(skB1=skB2))&(#i<#j))"	如果一笔交易由skA发送给skB1，并且在时间点#i被记录在门罗币的区块链上，则在时间点#i后不存在时间点#j使得该交易被再次发送给skB2并被确认上链，此时skB1与skB2不相等。

属性		验证结果
交易安全性	交易一致性	存在攻击路径
交易安全性	抗双花性	通过验证
不可追踪性	不可追踪性	存在攻击路径

基于Tamarin的门罗币支付协议分析方法

Analysis Method of Monero Payment Protocol Based on Tamarin

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献 22

相关文章 15

编辑推荐

Metrics

本文评价

[1]	文伟平, 张世琛, 王晗, 时林. 基于虚拟机自省的Linux恶意软件检测方案[J]. 信息网络安全, 2024, 24(5): 657-666.
[2]	李志华, 陈亮, 卢徐霖, 方朝晖, 钱军浩. 面向物联网Mirai僵尸网络的轻量级检测方法[J]. 信息网络安全, 2024, 24(5): 667-681.
[3]	杨志鹏, 王鹃, 马陈军, 亢云峰. 基于第三方库隔离的Python沙箱逃逸防御机制[J]. 信息网络安全, 2024, 24(5): 682-693.
[4]	顾国民, 陈文浩, 黄伟达. 一种基于多模型融合的隐蔽隧道和加密恶意流量检测方法[J]. 信息网络安全, 2024, 24(5): 694-708.
[5]	沈卓炜, 汪仁博, 孙贤军. 基于Merkle树和哈希链的层次化轻量认证方案[J]. 信息网络安全, 2024, 24(5): 709-718.
[6]	田钊, 牛亚杰, 佘维, 刘炜. 面向车联网的车辆节点信誉评估方法[J]. 信息网络安全, 2024, 24(5): 719-731.
[7]	石润华, 邓佳鹏, 于辉, 柯唯阳. 基于量子行走公钥加密的电子投票方案[J]. 信息网络安全, 2024, 24(5): 732-744.
[8]	郭建胜, 关飞婷, 李志慧. 一种带作弊识别的动态(t,n)门限量子秘密共享方案[J]. 信息网络安全, 2024, 24(5): 745-755.
[9]	张书雅, 陈良国, 陈兴蜀. 一种启发式日志模板自动发现方法[J]. 信息网络安全, 2024, 24(5): 767-777.
[10]	张长琳, 仝鑫, 佟晖, 杨莹. 面向网络安全领域的大语言模型技术综述[J]. 信息网络安全, 2024, 24(5): 778-793.
[11]	王巍, 胡永涛, 刘清涛, 王凯崙. 铁路运行环境下ERT可信根实体的软件化技术研究[J]. 信息网络安全, 2024, 24(5): 794-801.
[12]	郭梓萌, 朱广劼, 杨轶杰, 司群. 基于APT特征的铁路网络安全性能研究[J]. 信息网络安全, 2024, 24(5): 802-811.
[13]	张浩, 谢大智, 胡云晟, 叶骏威. 基于半监督学习的网络异常检测研究综述[J]. 信息网络安全, 2024, 24(4): 491-508.
[14]	王健, 陈琳, 王凯崙, 刘吉强. 基于时空图神经网络的应用层DDoS攻击检测方法[J]. 信息网络安全, 2024, 24(4): 509-519.
[15]	屠晓涵, 张传浩, 刘孟然. 恶意流量检测模型设计与实现[J]. 信息网络安全, 2024, 24(4): 520-533.