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

Analysis Method of Monero Payment Protocol Based on Tamarin

作　　者：李雨昕 黄文超[1] 王炯涵 熊焰[1] LI Yuxin;HUANG Wenchao;WANG Jionghan;XIONG Yan(School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China)

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026

出　　处：《信息网络安全》2024年第5期756-766,共11页Netinfo Security

基　　金：国家自然科学基金[62372422,61972369,62102385];安徽省自然科学基金[2108085QF262];中央高校基本科研业务费专项资金[WK2150110024]。

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

关 键 词：门罗币 TAMARIN 支付协议 符号模型 

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