We study distributed zero-knowledge proofs, introduced by Bick, Kol, and Oshman (SODA 2022). While distributed interactive proofs have advanced rapidly, general-purpose techniques for distributed zero-knowledge remain limited and mostly problem-specific. We address this gap by introducing distributed statistical zero-knowledge, requiring that each node's view be simulatable within negligible statistical distance, and by lifting the classical Sumcheck protocol (Lund, Fortnow, Karloff, and Nisan, FOCS 1990) into a modular primitive for distributed zero-knowledge proofs. Our main contribution is a distributed zero-knowledge implementation of Sumcheck. Given oracle access to a polynomial F over a finite field $\mathbb{F}$ with N variables, we design a protocol verifying claims of the form $\sum_{x\in\mathbb{F}} F(x)=a$ using $O(N)$ rounds of $O(\log |\mathbb{F}|)$-bit messages, while achieving statistical zero-knowledge and small soundness error. We apply this primitive to two problems. For non-k-colorability, we obtain an $O(n)$-round distributed statistical zero-knowledge proof deciding whether a graph is not k-colorable, for any constant k, using $O(log^{1+o(1)} n)$-bit messages. This is the first nontrivial distributed interactive proof for this problem, even without zero-knowledge guarantees. For Subgraph Counting, we obtain an $O(k \log n)$-round, $O(k \log n)$-bit distributed statistical zero-knowledge proof for counting copies of a given k-node pattern, improving previous distributed interactive proofs while additionally providing statistical zero-knowledge. Finally, we show that additional round compression of Sumcheck is problem-dependent: for non-3-colorability on constant-degree graphs, we prove a lower bound excluding $o(n/\log n)$ rounds under polynomial-time local computation.
With the widespread adoption of cryptocurrencies, the ability to conduct continuous offline payments has increasingly become a critical technological requirement. In network-constrained scenarios, current dual-offline payment technologies are useful for single transactions. However, their limitations in continuous payment scenarios have become increasingly evident, making them unable to meet real-world application needs. This has prompted the industry to demand more urgent innovations in research on continuous offline payment capabilities. To address these challenges, this paper proposes a continuous dual-offline payment system capable of supporting multiple continuous payments. The system integrates elliptic curve cryptography (ECC) and zero-knowledge proof (ZKP) technology to generate secure asset credentials, ensuring both immutability and privacy credentials throughout the offline payment lifecycle. A dynamic credential decomposition mechanism enables the splitting of input credentials into change credentials and receipt credentials, facilitating uninterrupted dual-offline payments between hardware wallets. Additionally, it incorporates a batch verification scheme based on smart contracts, utilizing zero-balance verification and chained hash tracing to ensure payment uniqueness and prevent double-spending attacks, thereby guaranteeing the verifiability and validity of payment settlements. Experimental evaluations demonstrate that the proposed system reduces gas consumption per payment and improves execution efficiency during batch processing, combining high security with strong performance. This research provides a feasible solution for the application of digital currencies in offline scenarios, carrying significant theoretical value and practical significance for driving technological innovation and application expansion in the cryptocurrency field. In addition to cryptocurrency payments, the proposed system is also applicable to IoT and sensor network environments. Many IoT devices operate in disconnected or network-limited areas and require secure micro-transactions. Our dual-offline payment mechanism supports such scenarios, as the main cryptographic operations are lightweight enough for typical IoT hardware. This further extends the practical value of our system beyond traditional cryptocurrency payments.
Vote Chain is a fully implemented, decentralized e-voting application (DApp) built on Ethereum. Existing blockchain-based voting systems often suffer from either high computational overhead due to homomorphic encryption or lack of fully deployable, adversarially tested implementations. To address these limitations, VoteChain employs a keccak256-based commit–reveal protocol to preserve ballot secrecy during the voting phase, with Solidity 0.8.20 smart contracts enforcing all election rules autonomously. Wallet-based authentication via MetaMask eliminates centralized identity management. The system is validated through 14 automated unit tests (all passing in 615 ms) covering correctness, access control, double-voting, hash forgery, and phase-bypass attacks. Per-voter gas cost is approximately 120,000 units (commit and reveal combined). An ablation study confirms the non-redundant contribution of each architectural component. Comparative analysis shows that VoteChain achieves vote privacy without homomorphic encryption while maintaining full decentralization and implementation completeness. The system is evaluated and validated on a local Hardhat network, with the architecture readily extensible to Layer-2 rollups for large-scale elections.
Federated Learning (FL) enables collaborative model training while preserving data privacy but relies on centralized aggregation servers, leading to issues such as lack of transparency, vulnerability to malicious updates, and single points of failure. This paper proposes a decentralized federated learning framework integrating blockchain technology and the InterPlanetary File System (IPFS) to eliminate central authority and enhance trust. Smart contracts deployed on the Ethereum Sepolia testnet manage model submission, validation, incentive distribution, and reputation tracking. Model updates are stored off-chain using IPFS, while their hashes are recorded on the blockchain to ensure integrity and immutability. A staking and slashing mechanism is introduced to encourage honest participation, where valid contributions are rewarded and malicious updates are penalized. A reputation system further evaluates participant reliability over time. The system is implemented using PyTorch, Solidity, Web3.py, and React.js. Experimental results demonstrate improved security, transparency, and efficient decentralized coordination, highlighting the feasibility of integrating federated learning with blockchain and decentralized storage for scalable and trustworthy machine learning applications.
Umar . Abubakar, Hamza Itopa Sanni, Abdulsalam Aliyu
Conventional attendance management approaches in academic and organisational settings face persistent challenges that include susceptibility to proxy attendance, inadequate protection of biometric credentials, and the absence of privacy-preserving verification mechanisms in cloud-hosted deployments. This paper presents SecureAttend, a cloud-based attendance management framework that addresses these deficiencies through the integration of Zero-Knowledge Proof (ZKP) cryptographic authentication with biometric capture via a ZKTeco K40 Pro fingerprint terminal. The proposed framework employs a challenge-response ZKP protocol that enables users to demonstrate possession of valid authentication credentials without disclosing underlying private keys or biometric templates to the server. Attendance records are encrypted using AES-256 prior to storage in a MongoDB cloud database, while SHA-256 hashing provides tamper-evidence for each record. Session integrity is maintained through JWT-based token management, and access boundaries are enforced via a Role-Based Access Control (RBAC) policy. Functional evaluation across eighteen test scenarios confirmed complete compliance with stated requirements. Security assessment validated correct operation of cryptographic mechanisms, access controls, and audit logging subsystems. Performance benchmarks recorded average API response latencies of approximately 85 milliseconds for authentication requests and 120 milliseconds for attendance marking operations. The results demonstrate that ZKP authentication can be deployed effectively in real-world attendance management contexts, offering measurable improvements in privacy, integrity, and resistance to credential-based attacks compared with conventional approaches.
Cryptography is the backbone of modern network security, providing confidentiality, integrity, authentication, and non-repudiation for digital communication. However, the rapid evolution of cyber threats, particularly the looming arrival of large-scale quantum computers, poses serious challenges to the cryptographic algorithms that protect today's networks. This paper presents a systematic review of cryptography in network security, following the PRISMA 2020 guidelines. A total of 68 studies published between 2016 and 2025 were selected from five major academic databases: IEEE Xplore, ACM Digital Library, Scopus, Web of Science, and ScienceDirect. The review covers classical symmetric and asymmetric algorithms, widely deployed cryptographic protocols such as TLS 1.3, IPsec, and SSH, and the growing body of work on post-quantum cryptography (PQC). Key findings include the following: NIST finalized three post-quantum cryptographic standards (FIPS 203, 204, and 205) in August 2024; lightweight cryptography standards for IoT devices were published in 2025 with the selection of ASCON; and real-world deployment of hybrid classical/post-quantum schemes has already begun in major web browsers and messaging applications. This paper also examines emerging trends in homomorphic encryption, zero-knowledge proofs, and AI-driven cryptanalysis. Based on the findings, this review identifies critical gaps in PQC migration strategies, IoT security, and the integration of cryptography with artificial intelligence, and proposes directions for future research.
Swati Sachan, Dale Fickett, Richard Buchinger, Theo Miller
Recent advances in error-corrected qubits have accelerated the timeline for practical quantum computing. It poses a threat to cryptographic primitives used to secure financial systems, government infrastructure, communication networks, and DeFi (Decentralized Finance) ecosystems. This paper introduces a post-quantum secure federated DeFi framework that enables inter-bank collaboration to improve the inclusivity of individuals underserved by local lenders due to limited financial histories. Multiple banks contribute encrypted information batches to a virtual server, where lattice-based Fully Homomorphic Encryption (FHE) enables end-to-end homomorphic computation. The server fuses local data-driven probabilistic assessments, expert beliefs, and verifiable evidence generated by the NASA-IBM Prithvi Geospatial Foundation Model (GFM), in encrypted format. Decentralized technologies are employed to ensure tamper-proof evidence and auditable accountability for all encrypted data exchanges between institutions and the server. The framework is tested on agricultural lending decisions for rural borrowers in Virginia.
In this paper, we examine the patterns and determinants of cross-border cryptocurrency flows. While our analysis focuses primarily on Bitcoin flows, the cryptocurrency with the largest market capitalization, we show that our key results also extend to four major stablecoins. After documenting global patterns of cross-border Bitcoin flows and contrasting them with those of traditional capital flows, we employ a cross-country panel approach to identify the key drivers of cross-border crypto flows for up to 162 countries. Our results provide evidence for the presence of multiple coexisting motives. The most significant motives comprise strategies to adjust to unfavorable macro and financial developments, as well as the need to conduct international payment and remittance transfers. Moreover, by conducting a case study of cross-border Bitcoin flows after the COVID-19 shock, we find that these motives were particularly relevant at a time when economic conditions were weak and the need for remittances appeared high. Gaining a better understanding of the motives behind cross-border cryptocurrency transactions is crucial for informing the public debate on cryptocurrencies and their potential use cases.
A non-custodial threshold instrument for Bitcoin would allow value to transfer between parties without network connectivity, fees, or custodial dependency. Digital signatures and multisignature scripts provide part of the solution, but the core benefit is lost if the issuer retains a key capable of unilateral redemption. All prior multisignature schemes have positioned the issuer at or above the spending threshold. We propose a system that inverts this: the holder receives the two keys constituting the spending threshold of a 2-of-3 multisignature script, and the issuer holds one key arithmetically below it.
Paul Gerhart, Jay Taylor, Sri Aravinda Krishnan Thyagarajan
Atomic swaps are a fundamental primitive for the trustless exchange of digital assets across blockchains: they guarantee that either both parties receive the agreed assets or neither party transfers. While this all-or-nothing guarantee is powerful, it also imposes an inherent determinism that rules out exchanges whose intended outcome is probabilistic. As a result, existing atomic swaps cannot realize trustless exchanges in which one party pays for a fixed chance of receiving a larger asset or reward, as in lotteries, randomized allocation mechanisms, and probabilistic cross-chain trades. We introduce probabilistic swaps, a new cryptographic primitive that extends atomic swaps to the probabilistic setting. In a probabilistic swap, one party's transfer is executed with a fixed, publicly specified probability embedded in the protocol and cannot be biased by either party. This yields a trustless mechanism for randomized exchange with verifiable odds and no trusted intermediary. Our construction combines adaptor signatures with oblivious pseudorandom functions (OPRFs) to realize the desired probabilistic outcome while ensuring that neither party can predict or bias it in advance. Along the way, we introduce a new mechanism for the atomic exchange of OPRF evaluations for payments, which may be of independent interest. A key feature of our approach is that it preserves the minimal on-chain footprint of modern atomic-swap protocols. The protocol relies only on standard Bitcoin scripts, such as digital signatures and timelocks, and is deployable on any blockchain that already supports atomic swaps. Consequently, probabilistic swaps are indistinguishable from ordinary on-chain transactions, which helps preserve privacy and fungibility. We provide formal security foundations and demonstrate practicality through a probabilistic swap in the Bitcoin testnet and in the Lightning Network.
Data valuation is a foundational task in data marketplaces, where a Shapley-value attribution determines how a buyer's payment is distributed among data providers. Typically, the marketplace operator runs this attribution alone, requiring participants and external auditors to trust scores they cannot independently recompute on the underlying private data. While zero-knowledge proofs (ZKPs) can theoretically reconcile this conflict between privacy and verifiability, existing ZK valuation systems fail to scale to real-world marketplace demands due to prohibitive proving times or the requirement to disclose validation cohorts. We present ZK-Value, a practical, end-to-end ZK data-valuation system. Our solution bridges the scalability gap through a fully co-designed architecture: (1) LSH-Shapley, a locality-based valuation primitive that replaces expensive pairwise distance metrics with per-bucket collision counts; (2) ZK-LSH-Shapley, a tailored ZKP protocol that drastically reduces witness size by encoding these counts into bucket-level histograms rather than naive per-pair tensors; and (3) structural proof-system optimizations, specifically super-oracle batching and sparsity skipping. Evaluated across 12 standard datasets, ZK-Value delivers valuation quality on par with state-of-the-art baselines (within 0.033 AUROC of exact KNN-Shapley), while generating proofs in seconds to minutes and outperforming specialized ZK baselines by 12.6x to 68.1x in proving time, with verification in under 4.6 s.
Sinchana Shetty, Tejaswini M R, Kiran Samantha D S, Vijaylaxmi H Manjunatha
Existing electronic voting platforms are persistently centralized repositories, introducing fundamental security challenged by vote manipulation, result falsification, limited weaknesses [1]. Blockchain technology has emerged as a compelling alternative, owing to its cryptographic permanence, data management. This paper proposes and evaluates a fully integrated blockchain-based electoral system built on the Ethereum network, leveraging Solidity smart contracts to address these systemic shortcomings. The proposed architecture adopts a decentralized three-tier design incorporating Web3.js communication bridges and cryptographic validation mechanisms that collectively guarantee immutability, transparency, and end-to-end verifiability throughout all electoral phases. The system incorporates hierarchical role-based access controls, real-time vote tallying, and comprehensive audit trail functionality, while preserving voter anonymity through pseudonymous addressing. Experimental results demonstrate transaction confirmation within 15–20 seconds, with a mean gas consumption of 0.0023 ETH per vote, confirming practical feasibility for medium-scale deployments. A comparative evaluation against conventional centralized e-voting solutions highlights measurable security full-stack Ethereum-based voting platform comprising Solidity improvements and the elimination of single points of failure, balanced against acceptable computational overhead.
Anonymous digital credentials allow a user to prove possession of an attribute that has been asserted by an identity issuer without the user revealing any extra information about themselves. For example, a user who has received a digital passport credential can prove their “age is <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>></mml:mo> <mml:mn>18</mml:mn> </mml:mrow> </mml:math> ” without revealing any other attributes such as their name or date of birth. Despite their clear application to privacy-preserving authentication, anonymous credential schemes have been difficult to deploy at scale. Part of the difficulty arises because schemes in the literature, such as BBS+, use new cryptographic primitives that require system-wide changes to existing issuer infrastructure. In addition, issuers often require digital identity credentials to be device-bound by incorporating the device’s secure element into the presentation flow. As a result, schemes like BBS+ require updates to the hardware on every user's device. We propose new ZK techniques which enable the construction of an anonymous credential scheme for the legacy Elliptic Curve Digital Signature Algorithm (ECDSA) signature scheme. By adding efficient ZK arguments for statements about SHA-256 and document parsing for ISO-standardized identity formats, we construct the first ZK proof of posession of a credential that can be deployed without changing any issuer processes, without changes to mobile devices, and without requiring non-standard cryptographic assumptions. Furthermore, our proof system itself only relies on SHA-256 as its complexity assumption. Producing ZK proofs about ECDSA signatures has been a bottleneck for other ZK proof systems because standardized curves such as P256 use finite fields which do not support efficient number theoretic transforms. We overcome this bottleneck by designing a ZK proof system around sumcheck and the Ligero argument system, by designing efficient methods for Reed-Solomon encoding over the required fields, and by designing specialized circuits for ECDSA. Our proofs for ECDSA can be generated in as little as <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>≈</mml:mo> <mml:mn>20</mml:mn> </mml:mrow> </mml:math> ms. When incorporated into a fully standardized identity protocol such as the ISO MDOC standard, our system can generate a zero-knowledge proof for the MDOC presentation flow in a few hundred ms on mobile devices. These advantages make our scheme a promising candidate for privacy-preserving digital identity applications.
The intersection of Artificial Intelligence (AI) and distributed systems has given rise to Federated Learning (FL), a paradigm that enables decentralized model training without compromising local data privacy. As organizational data silos grow, deploying complex machine learning models across highly distributed edge networks becomes a critical infrastructural challenge. Standard FL implementations suffer from severe vulnerabilities related to adversarial gradient updates and computational bottlenecks at the aggregation layer. This paper presents a novel, end-to-end distributed architecture that hardens FL pipelines using advanced cryptographic verification and optimized big data processing frameworks. We introduce a Zero-Knowledge Proof (ZKP) wrapper that cryptographically validates node computations before global aggregation, neutralizing model poisoning attacks without inspecting raw gradients. Additionally, we evaluate the system's performance using extreme gradient boosting models optimized for distributed edge execution. We formalize the mathematical transformation of the machine learning loss functions into Rank-1 Constraint Systems (R1CS) suitable for succinct verification. Extensive experimental results demonstrate that our hybrid architecture achieves a 94.2\% accuracy retention under adversarial conditions while maintaining scalable throughput across 1,000 parallel distributed nodes, effectively bridging the gap between rigorous cryptographic security and high-performance distributed AI.
While public blockchains provide transparent and auditable transaction histories, they inherently compromise user privacy. Existing privacy-enhancing protocols, such as those deployed on Ethereum, typically rely on succinct zero-knowledge proofs (zk-SNARKs) to obscure the transaction graph. However, implementing comparable cryptographic guarantees on high-throughput blockchains like Algorand is challenging due to strict per-call execution budgets and the state contention introduced by global Merkle accumulators. This paper presents Obscura, a decentralized, non-custodial privacy protocol tailored for constrained smart contract environments. Obscura achieves transaction anonymity using Linkable Spontaneous Anonymous Group (LSAG) signatures over the BN254 elliptic curve, verified entirely on-chain. To overcome limitations of the Algorand Virtual Machine (AVM), we introduce a novel state model that leverages Algorand's Box Storage for $O(1)$ commitment membership checks, eliminating the need for global Merkle accumulators, and a dynamic opcode-budget expansion mechanism via pooled inner application calls. Our implementation demonstrates that signer-ambiguous privacy is practical and efficient on Algorand without relying on trusted setups or succinct proofs. Obscura provides a robust privacy layer for transparent ledgers, bridging the gap between high-throughput blockchain architectures and the dual requirements of cryptographic privacy and selective auditability.
Digital contracts are formal agreements created, signed, stored, verified and executed through digital platforms. These contracts require long-term protection because they often contain legally, financially and organisationally sensitive information. However, classical cryptographic methods used in current digital contract systems may become vulnerable with advances in quantum computing. This paper focuses on Quantum Internet of Contracts (QIoCs) as a future direction for preparing digital contracts for the quantum era. It examines post-quantum cryptography, quantum communication, blockchain, smart contracts, digital identity, zero-knowledge proofs and risk-based migration strategies. The paper argues that QIoCs cannot rely on a single security method. Instead, they require a layered approach that combines quantum-resistant blockchain protocols, privacy-preserving data authentication, secure audit trails, legal governance and staged migration from classical systems to quantum-safe contract infrastructures. The paper highlights the need for legal acceptance, governance standards and real-world testing of proposed post-quantum models. Overall, the paper provides a review-based framework for building safer and more reliable digital contracts in a quantum-safe future.
Electronic Healthcare Records (EHRs) provide distributed access to patient and doctor information through pervasive cloud-based storage. As this data is highly sensitive, robust privacy measures are essential to mitigate adversarial impacts. To ensure optimal privacy across multiple shared EHRs, this article proposes a Session-dependent Zero Knowledge Proof Technique (SZKPT). The framework identifies privacy breaches using two truth values: the first representing optimal session closure, and the second reflecting verification at each sharing instance. Both truth values are validated through iterated session validations, which are managed using a deep learning paradigm. During training, different combinations of truth values are employed to maximize privacy during data sharing, while iterative processes train consecutive validation instances to improve breach detection. Truth values are continuously updated to reflect the session closure and the most recent privacy verification. In practice, if either truth value equals zero, the session is suspended; otherwise, if truth values are valid in consecutive iterations, data sharing is delegated to the authorized user. The process is repeatted at regular intervals with updated truth values, ensuring continuous monitoring and adaptive privacy protection. The proposed technique is rigorously evaluated using key performance metrics, including access verification, computational complexity, privacy breach detection, verification time, and access delegation time. Results demonstrate that SZKPT effectively balances privacy preservation with usability, providing a reliable, scalable, and efficient solution for secure EHR management in cloud-based healthcare systems.
Quantum computing’s accelerating trajectory threatens the cryptographic foundations of every major blockchain network. Recent research demonstrates that fewer than 500 000 physical qubits could break ECC-256 in approximately nine minutes, while expert surveys place a 28–49% probability of a cryptographically relevant quantum computer (CRQC) emerging within ten years. This paper presents a layered reference architecture for end-to-end quantum-resilient distributed ledger systems, making three contributions: (1) a structured threat analysis applying STRIDE across blockchain architectural layers and post-quantum cryptography (PQC) migration phases; (2) a seven-layer reference architecture with per-layer interface specifications and dependency graph; and (3) a multi-chain quantum readiness assessment covering twelve major networks with fintech-specific migration strategies for decentralised finance (DeFi), stablecoins, tokenised real-world assets (RWA), and decentralised identity (DID). A critical finding is that blockchain’s primary quantum risk is real-time signature forgery upon CRQC arrival, not retroactive harvest-now-decrypt-later (HNDL) attacks on signatures. Cross-chain bridges, data availability layers, and Lightning Network payment channels are identified as the most critically neglected quantum attack surfaces.
Digital identity management is a cornerstone of effective e-governance, yet centralized identity systems face critical challenges including single points of failure, data breaches, and lack of citizen control over personal information. This paper proposes a blockchain-based Self-Sovereign Identity (SSI) framework for e-governance that enables citizens to own, control, and selectively disclose their identity credentials without relying on centralized authorities. Built on Hyperledger Fabric with W3C Decentralized Identifier (DID) standards and Verifiable Credentials, the framework incorporates zero-knowledge proofs (ZKPs) for privacy-preserving authentication and smart contracts for automated credential verification. Performance evaluation on a 4-organization, 16-peer Hyperledger Fabric network demonstrates a throughput of 4,800 transactions per second with an average identity verification latency of 85 ms, suitable for citizen-scale e-governance applications. Security analysis confirms resistance to identity theft, Sybil attacks, man-in-the-middle attacks, and credential forgery, achieving resistance scores above 94% across all evaluated attack vectors. The framework provides a practical pathway for governments to modernize identity infrastructure while preserving citizen privacy and data sovereignty.
Healthcare data is among the most sensitive and frequently targeted information in the digital era. Existing centralised Electronic Health Record (EHR) systems are vulnerable to data breaches, unauthorised access, and single-point failures. This paper introduces a blockchain-based privacy-preserving framework for healthcare data management that integrates smart contracts, attribute-based encryption (ABE), and zero-knowledge proofs (ZKP) to ensure tamper-proof, role-gated data access. Our system is deployed on a permissioned Hyperledger Fabric network with a RESTful API gateway and a React-based patient portal. Experimental evaluations show that the proposed system achieves 99.2% access-control policy enforcement, reduces unauthorised access incidents to near zero, and maintains record retrieval latency under 180 ms at the 95th percentile. The framework also supports HIPAA and GDPR compliance through immutable audit trails and consent lifecycle management
Zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARKs) allow for elegant, privacy-preserving validation of computations. PLONK, a subclass of the zk-SNARKs, is certainly useful, but its complex interactions with permutation arguments, lookup tables, and blinding, among other considerations, make the protocol difficult to follow, let alone understand. This paper describes a framework centered around the core components of zk-SNARKs. In particular, we detail the construction of arithmetic gate constraints, representation of witness polynomials, and the Kate-Zaverucha-Goldberg (KZG) commitment scheme. By removing permutation proofs, lookup, and blinding, we aim to simplify the pedagogy of zk-SNARKs and preserve their essential properties of soundness and completeness. We describe a Python module from the ground up that demonstrates the generation and validation of proofs in a PLONK-modified zk-SNARK. We validate the framework and its foundations with a benchmark of a module generating and validating proofs in a PLONK-modified zk-SNARK. We validate the module against a circuit of 1,000 gates and demonstrate that the system correctly rejects all invalid witnesses. We illustrate the expected asymptotic behavior, with a pro tor of tight the module is quasi-linear, and verification, tight. We justify the foundations of the module and describe tight with zero private inputs. We have also bridged the gap between abstract zk-SNARK theoretical arguments and their practical implementation and research. We have provided a simple, empirically grounded mechanism that describes the key components of PLONK. We have done this in such a way that researchers, developers, and teachers can build on this base module and create production-ready systems without the abstraction.
This is Paper 6 of a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography; Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over $\mathbb{Z}_q$ for prime $q$, the foundation of NTT-based post-quantum cryptography, has lacked an analogous theory. We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields. Our key insight is the renewal argument: when a fresh random mask is applied between two pipeline stages, the intermediate wire becomes perfectly uniform regardless of Stage 1's security parameter. For two PF-PINI gadgets with parameters $k_1$ and $k_2$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k_2$), Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to $k_1$, creating a necessary condition for differential power analysis. We formalize both theorems in Lean 4 with 18 machine-checked proofs and zero sorry stubs. We formally bridge the algebraic and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to formally diagnose Microsoft's Adams Bridge PQC accelerator: its absence of fresh inter-stage masking leaves Barrett output wires non-uniform under the first-order probing model, the same architectural flaw that two independent empirical analyses [3, 4] and our own prior structural analysis [1] identified. Computational evidence further suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.