Analysis Method of Monero Payment Protocol Based on Tamarin

doi:10.3969/j.issn.1671-1122.2024.05.009

Abstract

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

CLC Number:

TP309

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.

Figures/Tables 6

References 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不相等。

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