Range arguments are a type of zero-knowledge proofs that aim to prove that a prover's committed value falls within a specified range for a verifier. Previously, most range arguments were constructed based on the DLOG assumption, and hence, exponentiation operation is required for proof generation and verification. In addition, it is generally known that splitting a zero-knowledge proof protocol into a preprocessing phase and an online phase makes computation after fixing the input efficient. Still, such protocol has yet to be known for range arguments. This paper proposes an efficient range arguments protocol with a preprocessing phase. Our proposal takes a new approach by using arithmetic circuits to express the constraints that the prover must prove. The prover (resp. verifier) can generate (resp. verify) a part of proof based on multiplication and addition operations instead of exponentiation operations. Our range argument is a generic construction that does not rely on any particular mathematical assumptions, which enables us to construct a post-quantum range argument. The implementation evaluation shows that the total computation time for the prover and verifier in the online phase is efficient compared to Bulletproofs, one of the state-of-the-art range proofs. Especially, the prover computation is efficient.
Abstract This paper introduces semi-competitive differential game logic $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , which enables verification of safety-critical applications that involve interactions between two agents. In $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> have individual goals that may overlap, leading to nonzero-sum games. This makes $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> solves the subtlety that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> . The relationship between $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> and zero-sum differential game logic $$\textsf {dG}\mathcal {L}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:mi>L</mml:mi> </mml:mrow> </mml:math> is discussed and the purpose of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> illustrated in a canonical example.
The seminal work of Goldreich and Krawczyk (SIAM Journal on Computing) shows that any constant-round public-coin interactive proof for languages not in <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mi mathvariant="sans-serif">B</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> </mml:mrow> </mml:mrow> </mml:math> cannot be black-box zero knowledge. Their result says nothing, however, about proofs (or arguments) of knowledge for languages in <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mi mathvariant="sans-serif">B</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> </mml:mrow> </mml:mrow> </mml:math>. As a special case, their work leaves open the question of whether Schnorr's protocol for proving knowledge of discrete logarithms in cyclic groups is black-box zero knowledge. In this work we focus on the zero knowledge of proofs of knowledge, centering on Schnorr's protocol as a prominent example. We prove two lower bounds, ruling out two different classes of simulators through which Schnorr's protocol can be proven zero knowledge: We prove that if a relation <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>ℛ</mml:mi> </mml:mrow> </mml:math> has a public-coin interactive proof of knowledge that is black-box zero knowledge and this protocol is compatible with the Fiat-Shamir transform in the random oracle model, then <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>ℛ</mml:mi> </mml:mrow> </mml:math> must be efficiently searchable. As an immediate corollary, we deduce that Schnorr's protocol cannot be black-box zero knowledge in groups in which discrete log is hard. We define a new class of simulators for Schnorr's protocol, which we call generic simulators. A generic simulator is one that works in any cyclic group, and does not use the representation of the specific group in which Schnorr's protocol is instantiated. We prove that Schnorr's protocol cannot have generic simulators. As an additional contribution, we generalize the original lower bound of Goldreich and Krawczyk, to prove that a language not in <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mi mathvariant="sans-serif">B</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> <mml:mi mathvariant="sans-serif">P</mml:mi> </mml:mrow> </mml:mrow> </mml:math> cannot have an interactive proof (not necessarily of knowledge) that is both black-box zero knowledge and compatible with the Fiat-Shamir transform in the random oracle model. In conjunction with recent works, this extends the Goldreich-Krawczyk lower bound to public-coin protocols that are not constant-round but have round-by-round soundness, including the parallel repetition of any public-coin interactive proof.
John C. Kolesar, Shan Ali, Timos Antonopoulos, Ružica Piskač
Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs’ correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crêpe , the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crêpe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crêpe on a suite of hundreds of regular expression equivalence proofs. Crêpe can validate large proofs in only a few seconds each.
Distributed certification is a set of mechanisms that allows an all-knowing prover to convince the units of a communication network that the network's state has some desired property, such as being 3-colorable or triangle-free. Classical mechanisms, such as proof labeling schemes (PLS), consist of a message from the prover to each unit, followed by one round of communication between each unit and its neighbors. Later works consider extensions, called distributed interactive proofs, where the prover and the units can have multiple rounds of communication before the communication among the units. Recently, Bick, Kol, and Oshman (SODA '22) defined a zero-knowledge version of distributed interactive proofs, where the prover convinces the units of the network's state without revealing any other information about the network's state or structure. In their work, they propose different variants of this model and show that many graph properties of interest can be certified with them. In this work, we define and study distributed non-interactive zero-knowledge proofs (dNIZK); these can be seen as a non-interactive version of the aforementioned model, and also as a zero-knowledge version of PLS. We prove the following: - There exists a dNIZK protocol for 3-coloring with O(log n)-bit messages from the prover and O(log n)-size messages among neighbors. - There exists a family of dNIZK protocols for triangle-freeness, that presents a trade-off between the size of the messages from the prover and the size of the messages among neighbors. - There exists a dNIZK protocol for any graph property in NP in the random oracle models, which is secure against an arbitrary number of malicious parties.
Orestis Melkonian, Wouter Swierstra, James Chapman, Sub Software Technology · 6 authors
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.
Ryan Lavin, Xuekai Liu, Hardhik Mohanty, L. E. J. Norman · 6 authors
Zero-knowledge proofs (ZKPs) enable computational integrity and privacy by allowing one party to prove the truth of a statement without revealing underlying data. Compared with alternatives such as homomorphic encryption and secure multiparty computation, ZKPs offer distinct advantages in universality and minimal trust assumptions, with applications spanning blockchain systems and confidential verification of computational tasks. This survey provides a technical overview of ZKPs with a focus on an increasingly relevant subset called zkSNARKs. Unlike prior surveys emphasizing algorithmic and theoretical aspects, we take a broader view of practical deployments and recent use cases across multiple domains including blockchain privacy, scaling, storage, and interoperability, as well as non-blockchain applications such as voting, authentication, timelocks, and machine learning. To support consistent comparison, we provide (i) a taxonomy of application areas, (ii) evaluation criteria including proof size, prover and verifier time, memory, and setup assumptions, and (iii) comparative tables summarizing key tradeoffs and representative systems. The survey also covers supporting infrastructure, including zero-knowledge virtual machines, domain-specific languages, libraries, and frameworks. While emphasizing zkSNARKs for their prevalence in deployed systems, we compare them with zkSTARKs and Bulletproofs to clarify transparency and performance tradeoffs. We conclude with future research and application directions.
The recent MIP*=RE theorem of Ji, Natarajan, Vidick, Wright, and Yuen shows that the complexity class MIP* of multiprover proof systems with entangled provers contains all recursively enumerable languages. Prior work of Grilo, Slofstra, and Yuen [FOCS '19] further shows (via a technique called simulatable codes) that every language in MIP* has a perfect zero knowledge (PZK) MIP* protocol. The MIP*=RE theorem uses two-prover one-round proof systems, and hence such systems are complete for MIP*. However, the construction in Grilo, Slofstra, and Yuen uses six provers, and there is no obvious way to get perfect zero knowledge with two provers via simulatable codes. This leads to a natural question: are there two-prover PZK-MIP* protocols for all of MIP*? In this paper, we show that every language in MIP* has a two-prover one-round PZK-MIP* protocol, answering the question in the affirmative. For the proof, we use a new method based on a key consequence of the MIP*=RE theorem, which is that every MIP* protocol can be turned into a family of boolean constraint system (BCS) nonlocal games. This makes it possible to work with MIP* protocols as boolean constraint systems, and in particular allows us to use a variant of a construction due to Dwork, Feige, Kilian, Naor, and Safra [Crypto '92] which gives a classical MIP protocol for 3SAT with perfect zero knowledge. To show quantum soundness of this classical construction, we develop a toolkit for analyzing quantum soundness of reductions between BCS games, which we expect to be useful more broadly. This toolkit also applies to commuting operator strategies, and our argument shows that every language with a commuting operator BCS protocol has a two prover PZK commuting operator protocol.
Zero-knowledge proofs (zk-Proofs) are communication protocols by which a prover can demonstrate to a verifier that it possesses a solution to a given public problem without revealing the content of the solution. Arbitrary computations can be transformed into an interactive zk-Proof so anyone is convinced that it was executed correctly without knowing what was executed on, having huge implications for digital currency. Despite this, interactive proofs are not suited for blockchain applications but novel protocols such as zk-SNARKs have made zero-knowledge ledgers like Zcash possible. This project builds upon Wolfram's ZeroKnowledgeProofs paclet and implements a zk-SNARK compiler based on Pinocchio protocol.
This paper extends the previous paper [6] by implementing two blockchain simulators of Solidity-style smart contracts – a simple and a complex one, using the interactive theorem prover Agda. In the previous article [6], we built a simple and complex abstract model of Solidity-style smart contracts in Agda. These models had many features, such as calling different smart contracts, supporting the ability to call different smart contracts, and providing simple and complex instructions. Because of the use of coalgebras for representing smart contracts they supported loops and conditionals, using the support of those features for coalgebraic programs in Agda. The complex model supported gas costs and pure functions, similar to the Solidity language.
ROCYS is a knowledge resource for practitioners, scientists, and researchers working in various fields of cyber security, hacking, digital forensics, cyber warfare, viruses and worms domain or critical infrastructure protection area.
We present a signature scheme based on the Syndrome-Decoding problem in rank metric. It is a construction from multi-party computation (MPC), using a MPC protocol which is a slight improvement of the linearized-polynomial protocol used in [Fen22], allowing to obtain a zero-knowledge proof thanks to the MPCitH paradigm. We design two different zero-knowledge proofs exploiting this paradigm: the first, which reaches the lower communication costs, relies on additive secret sharings and uses the hypercube technique [AMGH+22]; and the second relies on low-threshold linear secret sharings as proposed in [FR22]. These proofs of knowledge are transformed into signature schemes thanks to the Fiat-Shamir heuristic [FS86].
The increasing use of artificial intelligence algorithms, smart contracts, the internet of things, cryptocurrencies, and digital money highlights the need for secure and sustainable decentralized solutions. Currently, the blockchain technology serves as the backbone for most decentralized systems. However, the question of axiomatization of the blockchain theory in the first-order logic has been open until today, despite the efficient computational implementations of these systems. This did not allow one to formalize the blockchain structure, as well as to model and verify it using logical methods. This work introduces a finitely axiomatizable blockchain theory T that defines a class of blockchain structures K using the axioms of the first-order logic. The models of the theory T are well-known blockchain implementations with the proof of work consensus algorithm, including Bitcoin, Ethereum (PoW version), Ethereum Classic, and some others. By utilizing mathematical logic, we can study these models and derive new theorems of the theory T through automatic proofs. Also, the axiomatization of blockchain opens up new opportunities to develop blockchain-based systems that can help solve some of the open problems in the fields of artificial intelligence, robotics, cryptocurrencies, etc.
Abner F. B. Costa, Henrique Hepp, Murilo V. G. da Silva, Leandro M. Zatesko
The Hidden Subgroup Problem (HSP) generalises many problems that are candidates to be NP-intermediate. It was shown that the decision version of HSP belongs to the zero-knowledge complexity class HVPZK and that, if the size of the group is known, it also belongs to NISZK. We show that whenever we can sample uniformly at random elements of the group and of a set, with the same size of the group, that contains the image of the function that hides the subgroup, the problem is in NIPZK1 (i.e. NIPZK with perfect completeness). As a second contribution, we show that NIPZK1 has a complete promise problem that is a restricted version of a complete promise problem for the NIPZK class.
In classical planning, the aim is to find a sequence of deterministic actions leading from the initial to a goal state. In this work, we consider the scenario where a party who knows the solution to a planning task, called the prover, wants to convince a second party, the verifier, that it has the solution without revealing any information about the solution itself. This is relevant in domains where privacy is important, for example when plans contain sensitive information or when the solution should not be revealed upfront. We achieve this by introducing a zero-knowledge protocol for plan existence. By restricting ourselves to tasks with polynomially-bounded plan length, we are able to construct a protocol that can be run efficiently by both the prover and verifier. The resulting protocol does not rely on any reduction, has a constant number of rounds, and runs in time polynomial in the size of the task.
This PhD project proposes the theoretical and technological foundations of an approach for decentralized processing of streaming knowledge graphs, where autonomous reasoners may combine individual and collective processing of continuous data. These decentralized stream processors shall be capable of sharing not only data stream knowledge, but also processing duties, using collaboration and negotiation protocols. Moreover, commonly agreed semantic vocabularies will be used to address the high dynamicity of reasoners' knowledge and goals. The approach proposed in this project goes beyond previous works on stream reasoning, enabling the self-organization and coordination among distributed stream reasoners, based on techniques and principles inspired by Multi-Agent systems. On the one hand, it adds the ability to explicate processing goals, capabilities and knowledge, while on the other it exploits potential ways of interconnecting them in ways that expand their combined capacity/efficacy for managing highly dynamic flows of streaming knowledge. Through this approach, efficient local stream processors can establish cooperative processing schemes, respecting data privacy restrictions and data locality requirements through the exchange of streaming Knowledge Graphs.
We introduce semitopology, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points represent participants in a decentralised system, and open sets represent collections of participants that collectively have the authority to collaborate to update their local state; we call this an actionable coalition. Examples of actionable coalition include: majority stakes in proof-of-stake blockchains; communicating peers in peer-to-peer networks; and even pedestrians working together to not bump into one another in the street. Where actionable coalitions exist, they have in common that: collaborations are local (updating the states of the participants in the coalition, but not immediately those of the whole system); collaborations are voluntary (up to and including breaking rules); participants may be heterogeneous in their computing power or in their goals (not all pedestrians want to go to the same place); participants can choose with whom to collaborate; and they are not assumed subject to permission or synchronisation by a central authority. We develop a topology-flavoured mathematics that goes some way to explaining how and why these complex decentralised systems can exhibit order, and gives us new ways to understand existing practical implementations.
Standard probabilistic models face fundamental challenges such as data scarcity, a large hypothesis space, and poor data transparency. To address these challenges, we propose a novel probabilistic model of data-driven temporal propositional reasoning. Unlike conventional probabilistic models where data is a product of domain knowledge encoded in the probabilistic model, we explore the reverse direction where domain knowledge is a product of data encoded in the probabilistic model. This more data-driven perspective suggests no distinction between maximum likelihood parameter learning and temporal propositional reasoning. We show that our probabilistic model is equivalent to a highest-order, i.e., full-memory, Markov chain, and it can also be viewed as a hidden Markov model requiring no distinction between hidden and observable variables. We discuss that limits provide a natural and mathematically rigorous way to handle data scarcity, including the zero-frequency problem. We also discuss that a probability distribution over data generated by our probabilistic model helps data transparency by revealing influential data used in predictions. The reproducibility of this theoretical work is fully demonstrated by the included proofs.
Graham Cormode, Marcel Dall’Agnol, Tom Gur, Christopher W. Hickey
Streaming interactive proofs (SIPs) enable a space-bounded algorithm with one-pass access to a massive stream of data to verify a computation that requires large space, by communicating with a powerful but untrusted prover. This work initiates the study of zero-knowledge proofs for data streams. We define the notion of zero-knowledge in the streaming setting and construct zero-knowledge SIPs for the two main algorithmic building blocks in the streaming interactive proofs literature: the sumcheck and polynomial evaluation protocols. To the best of our knowledge all known streaming interactive proofs are based on either of these tools, and indeed, this allows us to obtain zero-knowledge SIPs for central streaming problems such as index, point and range queries, median, frequency moments, and inner product. Our protocols are efficient in terms of time and space, as well as communication: the verifier algorithm's space complexity is $\mathrm{polylog}(n)$ and, after a non-interactive setup that uses a random string of near-linear length, the remaining parameters are $n^{o(1)}$. En route, we develop an algorithmic toolkit for designing zero-knowledge data stream protocols, consisting of an algebraic streaming commitment protocol and a temporal commitment protocol.Our analyses rely on delicate algebraic and information-theoretic arguments and reductions from average-case communication complexity.
Interactive proofs (IPs) and arguments are cryptographic protocols that enable an untrusted prover to provide a guarantee that it performed a requested computation correctly. Introduced in the 1980s, IPs and arguments represented a major conceptual expansion of what constitutes a “proof” that a statement is true. Traditionally, a proof is a static object that can be easily checked step-by-step for correctness. In contrast, IPs allow for interaction between prover and verifier, as well as a tiny but nonzero probability that an invalid proof passes verification. Arguments (but not IPs) even permit there to be “proofs” of false statements, so long as those “proofs” require exorbitant computational power to find. To an extent, these notions mimic in-person interactions that mathematicians use to convince each other that a claim is true, without going through the painstaking process of writing out and checking a traditional static proof. Celebrated theoretical results from the 1980s and 1990s such as IP = PSPACE and MIP = NEXP showed that, in principle, surprisingly complicated statements can be verified efficiently. What is more, any argument can in principle be transformed into one that is zero-knowledge, which means that proofs reveal no information other than their own validity. Zero-knowledge arguments have a myriad of applications in cryptography. Within the last decade, general-purpose zero-knowledge arguments have made the jump from theory to practice. This has opened new doors in the design of cryptographic systems, and generated additional insights into the power of IPs and arguments (zero-knowledge or otherwise). There are now no fewer than five promising approaches to designing efficient, general-purpose zero-knowledge arguments. This survey covers these approaches in a unified manner, emphasizing commonalities between them.