Arthur Ramos, Anjolina Grisi de Oliveira, Ruy de Queiroz, Tiago M. L. de Veras
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.
Applies the Evidence-Based Subjective Logic (EBSL) framework to zero-knowledge reputation systems and decentralised identity. Demonstrates how reputation opinions that are provably correct can be published without revealing the underlying evidence graph, using the EZKL zkML framework for proof generation.
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo
Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.
Pedro Baptista, Bernardo Pacheco, Filipe Apolinário, João Silveira · 6 authors
Having the ability to prove your knowledge is essential for obtaining a job. In the programming field, applicants make claims about the programming languages they master, and it is up to the interviewer to check the veracity of those claims. The goal of this work is to facilitate this process by extracting important information from GitHub, such as the number of bytes programmed in each programming language. The user is then able to ask for a Zero Knowledge Proof which can be downloaded and sent to any entity which places trust on out platform. The proof is verifiable without the entity interacting with our platform and does not leak information about the users' GitHub. The obtained results are promising, even though proofs can take several minutes to generate, they can be verified in many devices, such as laptops and smartphones, which greatly increases the number of users who can use our platform.
AI-based Problem Solving and Planning
Logic, Reasoning, and Knowledge
Intelligent Tutoring Systems and Adaptive Learning
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.
Antoine Bak, Guilhem Jazeron, Pierre Galissant, Léo Perrin
In recent years, many hash functions have been introduced to satisfy the pressing need of some zero-knowledge protocols for such primitives allowing a low degree verification of their round function when arithmetized over a large field.While this can be achieved by restricting their sub-components to low-degree functions (and their inverse), the newest primitives in this category also leverage the intricacies of some proof systems to use “Split-and-Lookup” non-linear functions that essentially apply a small S-box in parallel over the binary representation of a field element.Such components excel at hindering attacks relying on polynomial system solving, but they offer poor security against statistical attacks. On the other hand, low degree monomials offer the opposite guarantees, being strong against statistical attacks. Several primitives have recently been proposed that combine such components in different ways in order to get the best from both.In this paper, we target such primitives by relying on the low degree components to allow a low-cost polynomial solving step. The weakness of Split-and-Lookups against linear attacks is used to simplify these systems, and their weakness against differential attacks is then used to propagate across many rounds the differential patterns obtained during polynomial solving. We instantiate this general approach by attacking round-reduced Monolith, and providing a distinguisher on full-round Skyscraper. These result then shed some light on how to best combine the different types of components to achieve the highest security.
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.
After successfully transitioning from proof-of-work to proof-of-stake, the Ethereum blockchain’s developer community has set an ambitious goal of achieving rapid block finalization, ideally completing it before the next block proposal, a concept known as single slot finality. Currently, block finalization on the ETH beacon chain takes ∼ 15 minutes to collect the attestation from the majority of the validators. The current protocol has several drawbacks, including slow finalization, high bandwidth usage and a rigid aggregation structure that is prone to failures. The challenge is collecting cryptographic signatures from close to a million validators distributed worldwide, connected to the network in 12 seconds without requiring high bandwidth internet connections from the peers in the network. This study presents an alternative scheme that has the potential to realize single-slot finality. Ours is a fully decentralized approach in which no node has a specific role, rendering it more robust than the current one. We simulate our heuristics on the Ethereum network topology and demonstrate that it can efficiently collect a million attestations from almost ten thousand physical nodes.
B S Rajeshwari, Shamanth K Murthy, S M, S P Shashank
Cross-Chain interoperability is one of the critical challenges in Blockchain technology, which enables seamless communication and asset transfers between different chains. Existing interoperability solutions such as atomic swaps, relay chains, notary schemes and blockchain bridges, often face security vulnerabilities, scalability limitations, and trust assumptions that hinder their efficiency. Zero-Knowledge Proofs (ZKPs) offer a promising approach to enhancing the security and privacy of interoperability mechanisms by enabling verification of computations without revealing the transaction details. This research paper explores existing Cross-Chain interoperability solutions, including the problem they address, such as atomicity, privacy, and decentralization, their implementation or methodology used and their drawbacks that need to be further optimized. Furthermore, the paper explores the integration of ZKPs in interoperability protocols, evaluating their potential to achieve trustless and privacy-preserving crosschain communication and conclude with the outline of future research directions to improve and optimize the current limitations and develop better solutions.
As Distributed Ledger Technologies (DLTs) mature, the inherent performance and scalability shortcomings of linearly structured blockchain designs become better understood. Protocols based on Directed Acyclic Graphs (DAGs) have been proposed to address such shortcomings. DAG-based protocols differ from traditional DLTs in the way they build and represent knowledge about transactions and relations between them. While traditional DLTs have straightforward homogeneous semantic attached to blocks and links between blocks, the semantic of vertices and edges in DAG-based protocols is nuanced and varied. In this work, we identify almost a dozen of knowledge-building dimensions in DAG-based DLTs, none of which have been studied before. Knowledge-building is important in DAG-based DLTs because of its significant impact on the size of the DAG, the pace at which new transactions are added, the finality of transactions, and so on. We analyze 40 DAG-based DLTs from this perspective, summarize our results in a taxonomy, and identify a number of research gaps.
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.
Zero Knowledge (ZK) proofs are protocols with growing applications in fields such as cryptography. They can be particularly difficult to design and thus have multiple domain-specific languages (DSLs) to aid a programmer in their construction. Analysis methods for these protocols are then typically language-specific, greatly limiting their utility. Most languages compile user code into a midpoint polynomial-circuit called a rank one constraint system (R1CS). We provide tools to analyse these R1CS circuits which hence have much broader applicability than existing tools. Specifically, we design and implement a tool for equivalence up to renaming and scaling, useful to avoid repeating a laborious step of the ZK process. As implemented, the tool can handle circuits on the order of millions of constraints. Additionally, we provide methods to extract a directed acyclic hierarchical structure via clustering to guide an automated property prover with recursive proving. Such a structure typically exists in DSL code but is lost when compiled to R1CS and is required to make larger circuits feasible to pass to a property prover. The guidance given by our clustering methods to the property prover Civer gave comparable results to the guidance of the original structure present in the code and finished in faster time.
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.
Blockchain technology has become a foundational component for constructing decentralized, secure, and immutable distributed systems. The consensus mechanism ensures that all nodes in a blockchain network reach agreement on a single version of truth, thereby maintaining data consistency across the distributed ledger. The earliest blockchain application, Bitcoin, adopts Proof of Work (PoW), which provides high security at the cost of substantial computational power and energy consumption. Ethereum employs Proof of Stake (PoS) to reduce energy consumption, though it introduces new challenges in the fairness of node selection. Practical Byzantine Fault Tolerance (PBFT) has gained significant attention for its ability to achieve more efficient consensus by reducing computational and energy demands. However, traditional PBFT still requires extensive message exchanges and voting among nodes, leading to significant communication overhead in large-scale networks. To address these limitations and further enhance the performance of PBFT, we propose the Comprehensive Trust-based PBFT (CTPBFT) algorithm. CT-PBFT reduces communication overhead by excluding nodes with low trust scores from the consensus process, thereby optimizing overall efficiency. We conducted a thorough analysis and simulation of CT-PBFT, and the results demonstrate that CT-PBFT outperforms traditional PBFT in terms of consensus latency and throughput. Moreover, CT-PBFT is more effective than other trust-based PBFT variants in swiftly eliminating Byzantine nodes, providing a robust and efficient solution for secure communication in distributed systems.
Martin Farkas, Balaźs Ádám Toldi, Bertalan Zoltán Péter, Imre Kocsis
In most domains where declarative policies are employed, it is typically the executor of the policy who performs policy evaluation, and not the subjects of policies. However, this approach has evident drawbacks from the trust, transparency and privacy aspects, especially when the subjects are natural persons. Building on recent developments in noninteractive zero-knowledge proofs and the technologies and standards supporting Self-Sovereign Indentity solutions, in this paper, we propose Self-Evaluated Policies, which move policy evaluation to the subject and leave the executor in a (zero-knowledge) proof-checking role. We present an SSI-based system model, propose a proof-tree-checking computational model for zero-knowledge proofs over the evaluations of Prolog-based policies, and describe a Circombased prototype.
This chapter delves into the question of whether it is possible to build Web3 platforms without the use of dedicated tokens. The chapter is divided into three major parts. The first part discusses the roles tokens play on Web3 platforms. The second part discusses the problems tokens can bring to a Web3 platform, and the last section discusses various ways Web3 platforms can minimize the use of tokens.