Reusable Formal Verification of DAG-based Consensus Protocols

• URL: http://arxiv.org/abs/2407.02167v1
• Date: Tue, 2 Jul 2024 11:19:12 GMT
• Title: Reusable Formal Verification of DAG-based Consensus Protocols
• Authors: Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotic,
• Abstract summary: DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. This paper presents a safety-proven formal specification of two DAG-based protocols.
• Score: 8.277981465630377
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. A DAG-based consensus protocol collaboratively constructs a partial order of blocks of transactions and produces linearly ordered blocks. The ubiquity and strategic importance of blockchains call for formal proof of the correctness of key components, namely, consensus protocols. This paper presents a safety-proven formal specification of two DAG-based protocols. Our specification highlights several dissemination, DAG construction, and ordering variations that can be combined to express the two protocols. The formalization requires a refinement approach for modeling the consensus. In an abstract model, we first show the safety of DAG-based consensus on leader blocks and then further refine the specification to encompass all blocks for all processes. The TLA+ specification for a given protocol consists of 492-732 lines, and the proof system TLAPS verifies 2025-2294 obligations in 6-8 minutes.

Related papers

• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  We study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols. Existing approaches for threshold cryptosystems introduce a latency overhead of at least one message delay for running the threshold cryptographic protocol. We propose a mechanism to eliminate this overhead for blockchain-native threshold cryptosystems with tight thresholds.
  arXiv  Detail & Related papers  (2024-07-16T20:53:04Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• Security of hybrid BB84 with heterodyne detection [0.0]
  Quantum key distribution (QKD) promises everlasting security based on the laws of physics. Recent hybrid QKD protocols have been introduced to leverage advantages from both categories. We provide a rigorous security proof for a protocol introduced by Qi in 2021, where information is encoded in discrete variables.
  arXiv  Detail & Related papers  (2024-02-26T19:00:01Z)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  We introduce for non-uniform messages a novel hybrid universal network coding cryptosystem (NU-HUNCC) We show that NU-HUNCC is information-theoretic individually secured against an eavesdropper with access to any subset of the links.
  arXiv  Detail & Related papers  (2024-02-13T12:12:39Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Provably Secure Commitment-based Protocols over Unauthenticated Channels [0.0]
  We build a theoretic security framework to cover protocols whose characteristics may not always concur with existing models for authenticated exchanges. We propose a number of Commitment-based protocols to establish a shared secret between two parties, and study their resistance over unauthenticated channels. This means analyzing the security robustness of the protocol itself, and its robustness against Man-in-the-Middle attacks.
  arXiv  Detail & Related papers  (2023-07-28T10:35:35Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  We propose a security verification framework for cryptographic protocols using machine learning. We create arbitrarily large datasets by automatically generating random protocols and assigning security labels to them. We evaluate the proposed method by applying it to verification of practical cryptographic protocols.
  arXiv  Detail & Related papers  (2023-04-26T02:37:43Z)
• Byzantine-Robust Federated Learning with Optimal Statistical Rates and Privacy Guarantees [123.0401978870009]
  We propose Byzantine-robust federated learning protocols with nearly optimal statistical rates. We benchmark against competing protocols and show the empirical superiority of the proposed protocols. Our protocols with bucketing can be naturally combined with privacy-guaranteeing procedures to introduce security against a semi-honest server.
  arXiv  Detail & Related papers  (2022-05-24T04:03:07Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  We study the performance of a practical continuous-variable (CV) quantum key distribution protocol. We focus on the Gaussian-modulated coherent-state protocol with heterodyne detection in a high signal-to-noise ratio regime. This allows us to study the performance for practical implementations of the protocol and optimize the parameters connected to the steps above.
  arXiv  Detail & Related papers  (2022-05-20T12:37:09Z)
• Round-robin differential phase-time-shifting protocol for quantum key distribution: theory and experiment [58.03659958248968]
  Quantum key distribution (QKD) allows the establishment of common cryptographic keys among distant parties. Recently, a QKD protocol that circumvents the need for monitoring signal disturbance, has been proposed and demonstrated in initial experiments. We derive the security proofs of the round-robin differential phase-time-shifting protocol in the collective attack scenario. Our results show that the RRDPTS protocol can achieve higher secret key rate in comparison with the RRDPS, in the condition of high quantum bit error rate.
  arXiv  Detail & Related papers  (2021-03-15T15:20:09Z)
• Twin-field quantum digital signatures [4.503555294002338]
  Digital signature is a key technique in information security, especially for identity authentications. Quantum digital signatures (QDSs) provide a considerably higher level of security, i.e., information-theoretic security.
  arXiv  Detail & Related papers  (2020-03-25T08:04:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.