Maxim Jourenko, Mario Larangeira, Kanta Kurazumi, Keisuke Tanaka
Abstract Blockchain-based systems, in particular cryptocurrencies, face a serious limitation: scalability. This holds, especially, in terms of the number of transactions per second. Several alternatives are currently being pursued by both the research and practitioner communities. One venue for exploration is on protocols that do not constantly add transactions on the blockchain and therefore do not consume the blockchain’s resources. This is done using off-chain transactions, i.e. , protocols that minimize the interaction with the blockchain, also commonly known as Layer-2 approaches. This work relates several existing off-chain channel methods, also known as payment and state channels, channel network construction methods, and other components such as channel and network management protocols, e.g. , routing nodes. All these components are crucial to keep the usability of the channel and are often overlooked. In this work, we propose a taxonomy for all the components of Layer-2. We provide extensive coverage of the state-of-the-art protocols available outline their respective approaches, and discuss their advantages and disadvantages.
Driven by the increasing demand for multi-party data computation, Private Set Intersection (PSI) has become a pivotal technique for secure data sharing and privacy preservation. Although several efficient two-party PSI protocols have been developed, multi-party scenarios continue to suffer from limited computational efficiency and inadequate security guarantees. To address this engineering challenge, this study aims to enhance the performance and security of multi-party PSI protocols. We introduce SM-MPSI, a multi-party PSI protocol built upon national cryptographic standards. This protocol integrates SM2 and SM3 cryptographic mechanisms, employs non-interactive zero-knowledge proofs for identity authentication, and leverages domestic secure cryptographic chips to accelerate core algorithms. Experimental comparisons with existing mainstream protocols demonstrate significant improvements in computational efficiency and system scalability, while preserving robust security guarantees. Furthermore, SM-MPSI achieves enhanced communication efficiency and reduced resource consumption in multi-party scenarios. This research offers technical contributions toward advancing China's efforts in independent innovation in privacy-preserving computing and cryptographic technologies, thereby laying a solid foundation for strengthening national cybersecurity capabilities.
This paper reconstructs zero-knowledge extensions on Solana as an architecture theory. Drawing on the existing ecosystem and on the author's prior papers and implementations as reference material, we propose a two-axis model that normalizes zero-knowledge (ZK) use by purpose (scalability vs. privacy) and by placement (on-chain vs. off-chain). On this grid we define five layer-crossing invariants: origin authenticity, replay-safety, finality alignment, parameter binding, and private consumption, which serve as a common vocabulary for reasoning about correctness across modules and chains. The framework covers the Solana Foundation's three pillars (ZK Compression, Confidential Transfer, light clients/bridges) together with surrounding components (Light Protocol/Helius, Succinct SP1, RISC Zero, Wormhole, Tinydancer, Arcium). From the theory we derive two design abstractions - Proof-Carrying Message (PCM) and a Verifier Router Interface - and a cross-chain counterpart, Proof-Carrying Interchain Message (PCIM), indicating concrete avenues for extending the three pillars.
The Internet of Medical Things (IoMT) transforms healthcare by enabling real-time monitoring of patient vitals, such as heart rate and glucose levels, but faces significant challenges in securing sensitive data against cyber threats and ensuring reliability in resource-constrained wearable devices, like low-power biosensors with limited computational capacity. The rise of quantum computing, particularly Shor algorithm, threatens to break traditional cryptographic methods (e.g., RSA, ECC) within 5–10 years by efficiently solving their underlying mathematical problems, endangering patient data confidentiality. Post-quantum cryptography (PQC), such as lattice-based schemes, offers resilience but demands high computational resources, challenging IoMT scalability. Unlike other PQC IoMT frameworks, such as those using NTRU, which prioritize computational simplicity but lack advanced privacy mechanisms, Q-PRADAX pioneers a secure, adaptive data aggregation framework, integrating Ring-LWE-based PQC for quantum-resilient confidentiality, compact zk-SNARK proofs for tamper-proof verification of patient vitals, and adaptive clustering for enhanced network reliability and scalability. Evaluated using OMNeT + + 6.0.3 with INET 4.5, Q-PRADAX achieves 94.5% diagnostic accuracy on ECG datasets, 100% tampering detection, and 99.9% packet delivery across 1000 devices in its Baseline scenario, with a security latency of 12.2 ms/packet and energy consumption of 0.38 mJ/packet on ARM Cortex-M4 devices (200 mAh). Outperforming existing IoMT solutions in security and fault tolerance, Q-PRADAX establishes a global standard for a secure, patient-centric IoMT ecosystem, redefining reliable healthcare delivery.
Chong Chen, Jiachi Chen, Lingfeng Bao, David F. Lo · 10 authors
Smart contract vulnerabilities, particularly improper Access Control that allows unauthorized execution of restricted functions, have caused billions of dollars in losses. GitHub hosts numerous smart contract repositories containing source code, documentation, and configuration files-these serve as intermediate development artifacts that must be compiled and packaged before deployment. Third-party developers often reference, reuse, or fork code from these repositories during custom development. However, if the referenced code contains vulnerabilities, it can introduce significant security risks. Existing tools for detecting smart contract vulnerabilities are limited in their ability to handle complex repositories, as they typically require the target contract to be compilable to generate an abstract representation for further analysis. This paper presents TRACE, a tool designed to secure non-compilable smart contract repositories against access control vulnerabilities. TRACE employs LLMs to locate sensitive functions involving critical operations (e.g., transfer) within the contract and subsequently completes function snippets into a fully compilable contract. TRACE constructs a function call graph from the abstract syntax tree (AST) of the completed contract. It uses the control flow graph (CFG) of each function as node information. The nodes of the sensitive functions are then analyzed to detect Access Control vulnerabilities. Experimental results demonstrate that TRACE outperforms state-of-the-art tools on an open-sourced CVE dataset, detecting 14 out of 15 CVEs. In addition, it achieves 89.2% precision on 5,000 recent on-chain contracts, far exceeding the best existing tool at 76.9%. On 83 real-world repositories, TRACE achieves 87.0% precision, significantly surpassing DeepSeek-R1's 14.3%.
Digital transactions currently exceed trillions of dollars annually, yet traditional paper-based agreements remain a bottleneck for automation, enforceability, and dispute resolution. Natural language contracts introduce ambiguity, require manual processing, and lack computational verifiability, all of which hinder efficient digital commerce. Computable legal contracts, expressed in machine-readable formats, offer a potential solution by enabling automated execution and verification. Blockchain-based smart contracts further strengthen enforceability and accelerate dispute resolution; however, current implementations risk exposing sensitive agreement terms on public ledgers, raising serious privacy and competitive intelligence concerns that limit enterprise adoption. We introduce zk-agreements, a protocol designed to transition from paper-based trust to cryptographic trust while preserving confidentiality. Our design combines zero-knowledge proofs to protect private agreement terms, secure two-party computation to enable private compliance evaluation, and smart contracts to guarantee automated enforcement. Together, these components achieve both privacy preservation and computational enforceability, resolving the fundamental tension between transparency and confidentiality in blockchain-based agreements.
This paper addresses the challenge of designing secure and private digital credentialing systems by leveraging advanced mathematical primitives from applied cryptography. The core of our proposed solution is the application of Zero-Knowledge Proofs (ZKPs), a class of cryptographic protocols that allows for the verification of assertions without disclosing the underlying secret data. We introduce a formal, layered architecture that demonstrates how the mathematical properties of ZKPs can be systematically translated into a robust, large-scale information system. The framework's design is validated against the complex requirements of the academic domain, which serves as a rigorous testbed for our architectural approach. The primary contribution is a blueprint for integrating complex cryptographic protocols into practical system design, demonstrating how mathematical guarantees of privacy can be preserved in a distributed and verifiable manner. This work provides a novel contribution at the intersection of applied cryptography, system architecture, and information security.
Abstract The increasing fragmentation of blockchain networks, compounded by recurring vulnerabilities in conventional cross-chain bridges—including censorship, replay attacks, and validator collusion—underscores an urgent need for secure and privacy-preserving interoperability protocols. This paper introduces ZK-InterChain, a protocol designed for unidirectional data transfers from consortium to public blockchains. The system empowers users to prove private or semi-private actions, such as verified purchases, without revealing their identities on the public network. The core of ZK-InterChain's architecture features a dual Zero-Knowledge Proof (ZKP) system. A client-side module facilitates user-generated proofs of private activity, while a validator-side module attests to state updates from the consortium chain using aggregated BLS signatures. Privacy is maintained through cryptographic nullifiers and minimal public inputs, which decouple a user's identity from their public-chain activities. Security analysis confirms the protocol's resilience against key attack vectors. Empirical evaluation demonstrates user-side proof generation in approximately one minute and validator-side state attestation in two minutes, with on-chain verification consuming approximately 220k gas. These performance characteristics establish ZK-InterChain as a viable solution for non-immediate, privacy-sensitive applications, such as decentralized reputation systems, post-event credentialing, and anonymous feedback mechanisms.
Iván Abellán Álvarez, Pol Hölzmer, Johannes Sedlmeir
Digital identity wallets promise significant advancements in digital identity management by offering users a high degree of convenience, security, and control over their data disclosure. However, there is also criticism regarding their privacy guarantees, especially when used in regulated use cases that require high levels of assurance on the correctness and binding of a legal identity. In this paper, we present a comprehensive privacy model and analysis of one of the most prominent digital wallets – the European Digital Identity Wallet (EUDIW) – as specified by the Architecture and Reference Framework (ARF) and the eIDAS 2.0 regulation. We employ a suite of qualitative privacy risk assessment methods to systematically map and evaluate information flows in three key use cases. Our analysis identifies multiple privacy risks – including linkability, identifiability, and excessive attribute data disclosure – and reveals that although the ARF is designed to comply with privacy-by-design principles, inherent design choices, such as the reliance on SD-JWT and mDOC data formats, as well as the concept of a Wallet Unit Attestation (WUA), retain risks to user privacy. Building on our findings, we then highlight how advanced Privacy-Enhancing Technologies (PETs), such as (general-purpose) Zero-Knowledge Proofs (ZKPs), can reduce or mitigate some of these risks.
Energy consumption in Federated Learning (FL) has emerged as a major challenge due to the growing deployment of intelligent edge devices and the increasing complexity of machine learning models. FL enables collaborative model training across decentralized data sources without transferring raw data, thereby reducing communication overhead and enhancing data privacy by design. These features make FL particularly suitable for applications in healthcare, finance, and industrial IoT, where data sensitivity and resource constraints are critical. This paper provides a comprehensive survey of energy-efficient techniques in FL, classifying them into four main categories: model compression (including pruning and quantization), communication optimization, client selection, and hardware-aware strategies. The paper presents a unified taxonomy and discusses the strengths, limitations, and trade-offs of each approach. A comparative evaluation framework is introduced to assess energy savings, model accuracy, communication cost, and deployment feasibility. By analyzing current trends and open challenges, this review offers valuable guidance for researchers and practitioners in the development of scalable, energy-aware, and privacy-preserving federated learning systems.
Abstract Blockchain wallet manages decentralized identities in Web3, which allows users to identify themselves in a verifiable yet anonymous manner by digital signatures. However, native wallet scheme has been proven vulnerable to Sybil attacks in practice, where adversaries can easily create large numbers of controlled wallets at a low cost to undermine Web3 applications. To this end, many solutions are proposed for mitigating Sybil attacks. Nevertheless, they typically rely on either costly specialized biometric hardware or behavior-based heuristics that can be easily bypassed. In this paper, we introduce EdenDID, the first trinity-bound identity management system that uniquely binds human user, wallet address, and physical device into a unified framework. EdenDID combines edge-based video recognition, on-chain transactional activity analysis, and device computational power verification to establish a decentralized Proof-of-Trustworthiness consensus. The system provides compliant users with a trusted, verifiable credential to prove their unique identity. We prototype low-cost Eden Devices and deploy them on a Layer-2 blockchain network. Our experiments demonstrate the low end-to-end latency and robust resistance performance to Sybil attacks. Moreover, we present a case study to show how EdenDID can mitigate virtual-hardware fraud in DePIN, in which EdenDID successfully binds the user, wallet, and device uniquely, thus preventing users from binding multiple wallets or devices.
Maximal Extractable Value (MEV) refers to a class of attacks to decentralized applications where the adversary profits by manipulating the ordering, inclusion, or exclusion of transactions in a blockchain. Decentralized Finance (DeFi) protocols are a primary target of these attacks, as their logic depends critically on transaction sequencing. To date, MEV attacks have already extracted billions of dollars in value, underscoring their systemic impact on blockchain security. Verifying the absence of MEV attacks requires determining suitable upper bounds, i.e. proving that no adversarial strategy can extract more value (if any) than expected by protocol designers. This problem is notoriously difficult: the space of adversarial strategies is extremely vast, making empirical studies and pen-and-paper reasoning insufficiently rigorous. In this paper, we present the first mechanized formalization of MEV in the Lean theorem prover. We introduce a methodology to construct machine-checked proofs of MEV bounds, providing correctness guarantees beyond what is possible with existing techniques. To demonstrate the generality of our approach, we model and analyse the MEV of two paradigmatic DeFi protocols. Notably, we develop the first machine-checked proof of the optimality of sandwich attacks in Automated Market Makers, a fundamental DeFi primitive.
This article explores the characteristics of data resources from the perspective of production factors, analyzes the demand for trustworthy circulation technology, designs a fusion architecture and related solutions, including multi-party data intersection calculation, distributed machine learning, etc. It also compares performance differences, conducts formal verification, points out the value and limitations of architecture innovation, and looks forward to future opportunities.
With the rapid adoption of diffusion models for visual content generation, proving authorship and protecting copyright have become critical. This challenge is particularly important when model owners keep their models private and may be unwilling or unable to handle authorship issues, making third-party verification essential. A natural solution is to embed watermarks for later verification. However, existing methods require access to model weights and rely on computationally heavy procedures, rendering them impractical and non-scalable. To address these challenges, we propose NoisePrints, a lightweight watermarking scheme that utilizes the random seed used to initialize the diffusion process as a proof of authorship without modifying the generation process. Our key observation is that the initial noise derived from a seed is highly correlated with the generated visual content. By incorporating a hash function into the noise sampling process, we further ensure that recovering a valid seed from the content is infeasible. We also show that sampling an alternative seed that passes verification is infeasible, and demonstrate the robustness of our method under various manipulations. Finally, we show how to use cryptographic zero-knowledge proofs to prove ownership without revealing the seed. By keeping the seed secret, we increase the difficulty of watermark removal. In our experiments, we validate NoisePrints on multiple state-of-the-art diffusion models for images and videos, demonstrating efficient verification using only the seed and output, without requiring access to model weights.
The integration of blockchain technology into healthcare presents a paradigm shift for secure data management, enabling decentralized and tamper-proof storage and sharing of sensitive Electronic Health Records (EHRs). However, existing blockchain-based healthcare systems, while providing robust access control, commonly overlook the high latency in user-side re-computation of hashes for integrity verification of large multimedia data, impairing their practicality, especially in time-sensitive clinical scenarios. In this paper, we propose FAITH, an innovative scheme for \underline{F}ast \underline{A}uthenticated and \underline{I}nteroperable mul\underline{T}imedia \underline{H}ealthcare data storage and sharing over hybrid-storage blockchains. Rather than user-side hash re-computations, FAITH lets an off-chain storage provider generate verifiable proofs using recursive Zero-Knowledge Proofs (ZKPs), while the user only needs to perform lightweight verification. For flexible access authorization, we leverage Proxy Re-Encryption (PRE) and enable the provider to conduct ciphertext re-encryption, in which the re-encryption correctness can be verified via ZKPs against the malicious provider. All metadata and proofs are recorded on-chain for public verification. We provide a comprehensive analysis of FAITH's security regarding data privacy and integrity. We implemented a prototype of FAITH, and extensive experiments demonstrated its practicality for time-critical healthcare applications, dramatically reducing user-side verification latency by up to $98\%$, bringing it from $4$ s down to around $70$ ms for a $5$ GB encrypted file.
The rapid growth of data-driven applications in healthcare, finance, IoT, and autonomous systems has created a pressing need for privacy-preserving and scalable machine learning methods. Traditional centralized learning, which aggregates data into a single repository, faces challenges related to data privacy, security, communication overhead, and regulatory compliance. Federated Learning (FL) offers a decentralized solution, enabling multiple clients to collaboratively train a global model without sharing raw data. Only model updates are exchanged, preserving privacy while leveraging distributed computational resources. This paper reviews FL architectures— including centralized, decentralized, horizontal, vertical, cross-device, and cross-silo—along with core components such as local clients, central servers, and communication protocols. Privacy- preserving techniques like differential privacy, secure aggregation, homomorphic encryption, and anonymization/pseudonymization are discussed to protect sensitive information. FL applications span healthcare, finance, IoT, smart devices, and autonomous systems, highlighting its transformative potential. Key challenges include data and system heterogeneity, efficient aggregation, personalization, robustness, and regulatory compliance. Future directions focus on enhanced privacy, communication efficiency, model personalization, and integration with edge and IoT environments. FL thus represents a promising paradigm for secure, collaborative, and distributed artificial intelligence.
Jonas Gebele, Timm Mutzel, Burak Oez, Florian Matthes
Sealed-bid auctions ensure fair competition and efficient allocation but are often deployed on centralized infrastructure, enabling opaque manipulation. Public blockchains eliminate central control, yet their inherent transparency conflicts with the confidentiality required for sealed bidding. Prior attempts struggle to reconcile privacy, verifiability, and scalability without relying on trusted intermediaries, multi-round protocols, or expensive cryptography. We present a sealed-bid auction protocol that executes sensitive bidding logic on a Trusted Execution Environment (TEE)-backed confidential compute blockchain while retaining settlement and enforcement on a public chain. Bidders commit funds to enclave-generated escrow addresses, ensuring confidentiality and binding commitments. After the deadline, any party can trigger resolution: the confidential blockchain determines the winner through verifiable off-chain computation and issues signed settlement transactions for execution on the public chain. Our design provides security, privacy, and scalability without trusted third parties or protocol modifications. We implement it on SUAVE with Ethereum settlement, evaluate its scalability and trust assumptions, and demonstrate deployment with minimal integration on existing infrastructure.
Electronic voting (e-voting) has become an essential topic in the modernization of democratic systems, with promises of accessibility, faster counting, and reduced logistical challenges compared to traditional paper ballots. Yet, widespread adoption has been hindered by persistent trust and security concerns. Vulnerabilities such as malware, server compromise, insider threats, and limited verifiability have generated skepticism regarding the integrity of e-voting platforms. Blockchain technology has emerged as a disruptive innovation capable of reshaping this discourse. Its intrinsic properties—immutability, decentralization, transparency, and consensus-driven validation—directly address many of the fundamental challenges associated with securing digital elections. This manuscript provides a comprehensive exploration of blockchain-based electronic voting, with particular emphasis on the trust and security challenges that shape its practical deployment. Drawing on global case studies, theoretical models, and simulation insights, the research examines how blockchain can ensure tamper resistance, facilitate end-to-end verifiability, and empower voters through transparent audit trails. Key challenges such as scalability bottlenecks, voter anonymity risks, usability barriers, and regulatory gaps are analyzed in depth. The results indicate that hybrid blockchain architectures, which integrate advanced cryptographic techniques such as zero-knowledge proofs, homomorphic encryption, and sharding, hold promise for balancing the competing demands of scalability, privacy, and trust. Furthermore, blockchain must be supported by strong institutional frameworks, inclusive accessibility measures, and continuous technical audits to achieve legitimacy in electoral processes. By systematically mapping both the opportunities and limitations, this research contributes to the ongoing discourse on how technology can strengthen democratic resilience in the digital era. Ultimately, blockchain-enabled voting should be regarded not as a replacement but as an augmentation of existing systems, combining the strengths of distributed technologies with constitutional safeguards to advance secure, transparent, and inclusive electoral participation.
Alison Gonçalves Schemitt, Henrique Fan da Silva, Roben Castagna Lunardi, Diego Kreutz · 6 authors
The advent of quantum computing poses a threat to the security of traditional encryption algorithms. This has motivated the development of post-quantum cryptography (PQC). In 2024, the National Institute of Standards and Technology (NIST) standardized several PQC algorithms, marking an important milestone in the transition toward quantum-resistant security. Blockchain systems fundamentally rely on cryptographic primitives to guarantee data integrity and transaction authenticity. However, widely used algorithms such as ECDSA, employed in Bitcoin, Ethereum, and other networks, are vulnerable to quantum attacks. Although adopting PQC is essential for long-term security, its computational overhead in blockchain environments remains largely unexplored. In this work, we propose a methodology for benchmarking both PQC and traditional cryptographic algorithms in blockchain contexts. We measure signature generation and verification times across diverse computational environments and simulate their impact at scale. Our evaluation focuses on PQC digital signature schemes (ML-DSA, Dilithium, Falcon, Mayo, SLH-DSA, SPHINCS+, and Cross) across security levels 1 to 5, comparing them to ECDSA, the current standard in Bitcoin and Ethereum. Our results indicate that PQC algorithms introduce only minor performance overhead at security level 1, while in some scenarios they significantly outperform ECDSA at higher security levels. For instance, ML-DSA achieves a verification time of 0.14 ms on an ARM-based laptop at level 5, compared to 0.88 ms for ECDSA. We also provide an open-source implementation to ensure reproducibility and to encourage further research.
Zero-knowledge proof (ZKP) applications require translating high-level programs into arithmetic circuits–a process that demands both correctness and efficiency. While recent DSLs improve usability, they often yield suboptimal circuits, and hand-optimized implementations remain difficult to construct and verify. We present Tabby, a synthesis-aided compiler that automates the generation of high-performance ZK circuits from highlevel code. Tabby introduces a domain-specific intermediate representation designed for symbolic reasoning and applies sketch-based program synthesis to derive optimized low-level implementations. By decomposing programs into reusable components and verifying semantic equivalence via SMT-based reasoning, Tabby ensures correctness while achieving substantial performance improvements. We evaluate Tabby on a suite of real-world ZKP applications and demonstrate significant reductions in proof generation time and circuit size against mainstream ZK compilers.
Decentralized applications (dApps) in Decentralized Finance (DeFi) face a fundamental tension between regulatory compliance requirements like Know Your Customer (KYC) and maintaining decentralization and privacy. Existing permissioned DeFi solutions often fail to adequately protect private attributes of dApp users and introduce implicit trust assumptions, undermining the blockchain's decentralization. Addressing these limitations, this paper presents a novel synthesis of Self-Sovereign Identity (SSI), Zero-Knowledge Proofs (ZKPs), and Attribute-Based Access Control to enable privacy-preserving on-chain permissioning based on decentralized policy decisions. We provide a comprehensive framework for permissioned dApps that aligns decentralized trust, privacy, and transparency, harmonizing blockchain principles with regulatory compliance. Our framework supports multiple proof types (equality, range, membership, and time-dependent) with efficient proof generation through a commit-and-prove scheme that moves credential authenticity verification outside the ZKP circuit. Experimental evaluation of our KYC-compliant DeFi implementation shows considerable performance improvement for different proof types compared to baseline approaches. We advance the state-of-the-art through a holistic approach, flexible proof mechanisms addressing diverse real-world requirements, and optimized proof generation enabling practical deployment.
Computer-aided cryptography, with particular emphasis on formal verification, promises an interesting avenue to establish strong guarantees about cryptographic primitives. The appeal of formal verification is to replace the error-prone pen-and-paper proofs with a proof that was checked by a computer and, therefore, does not need to be checked by a human. In this paper, we ask the question of how reliable are these machine-checked proofs by analyzing a formally verified implementation of the Line-Point Zero-Knowledge (LPZK) protocol (Dittmer, Eldefrawy, Graham-Lengrand, Lu, Ostrovsky and Pereira, CCS 2023). The implementation was developed in EasyCrypt and compiled into OCaml code that was claimed to be high-assurance, i.e., that offers the formal guarantees of guarantees of completeness, soundness, and zero knowledge. We show that despite these formal claims, the EasyCrypt model was flawed, and the implementation (supposed to be high-assurance) had critical security vulnerabilities. Concretely, we demonstrate that: 1) the EasyCrypt soundness proof was incorrectly done, allowing an attack on the scheme that leads honest verifiers into accepting false statements; and 2) the EasyCrypt formalization inherited a deficient model of zero knowledge for a class of non-interactive zero knowledge protocols that also allows the verifier to recover the witness. In addition, we demonstrate 3) a gap in the proof of the perfect zero knowledge property of the LPZK variant of Dittmer, Ishai, Lu and Ostrovsky (CCS 2022) that the EasyCrypt proof is based, which, depending on the interpretation of the protocol and security claim, could allow a malicious verifier to learn the witness. Our findings highlight the importance of scrutinizing machine-checked proofs, including their models and assumptions. We offer lessons learned for both users and reviewers of tools like EasyCrypt, aimed at improving the transparency, rigor, and accessibility of machine-checked proofs. By sharing our methodology and challenges, we hope to foster a culture of deeper engagement with formal verification in the cryptographic community.
Traceable Ring Signatures (TRS) were introduced by Fujisaki and Suzuki~[PKC'07], where a trace algorithm can publicly check if two signatures with the same event label were generated by the same signer (linkability). In addition, if the two signatures correspond to different messages, then the signer's identity is revealed (traceability). Following [PKC'07], most subsequent works adopt the same definitions and consider three security properties, anonymity, linkability, and exculpability. [PKC'07] proved that the latter two properties together imply unforgeability, a fundamental requirement for all signature-like primitives. ~~~~In this work, we identify a gap in the aforementioned proof, which arises from the insufficient consideration of linkability and exculpability in [PKC'07]. To address this, we revisit the syntax and security notions of TRS, and close this gap by defining extended linkability and extended exculpability. Building on these, we design a new framework of TRS from PseudoRandom Functions (PRF) and Zero-Knowledge Proofs of Knowledge (ZKPoK) that supports tracing, provided that both two signatures are valid. This constitutes a substantial improvement over existing approaches---all of which require tracing with the size of the ring---and elevates TRS to a level of practicality and efficiency comparable to Linkable Ring Signatures (LRS), which have already achieved widespread deployment in practice. Finally, we instantiate our generic framework from the DDH assumption and leverage the Bulletproofs [S\&P'18] to construct a TRS scheme with log-size signatures. The proposed scheme achieves highly optimized signature sizes in practice and remains compatible with most existing DLog-based systems. On Curve25519, the signature size is bytes, which to our best knowledge is the shortest LRS scheme for a ring .