2020/09/22 by Joel Wanner, Wanner, Joel, Laurent Chuat +3
Computer Science · Decision Sciences · #Cryptography and Security (cs.CR) #Data Quality and Management #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Parallel #Service-Oriented Architecture and Web Services #and Cluster Computing (cs.DC) #cs.CR #cs.DC
paper · pdf · doi:10.48550/arxiv.2009.10664
International Symposium on Reliable Distributed Systems (SRDS) 2020
arxiv created 2020/09/22 · openalex publication_date 2020/09/22 · arxiv updated 2020/09/23 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Byzantine fault tolerant protocols enable state replication in the presence of crashed, malfunctioning, or actively malicious processes. Designing such protocols without the assistance of verification tools, however, is remarkably error-prone. In an adversarial environment, performance and flexibility come at the cost of complexity, making the verification of existing protocols extremely difficult. We take a different approach and propose a formally verified consensus protocol designed for a specific use case: secure logging. Our protocol allows each node to propose entries in a parallel subroutine, and guarantees that correct nodes agree on the set of all proposed entries, without leader election. It is simple yet practical, as it can accommodate the workload of a logging system such as Certificate Transparency. We show that it is optimal in terms of both required rounds and tolerable faults. Using Isabelle/HOL, we provide a fully machine-checked security proof based upon the Heard-Of model, which we extend to support signatures. We also present and evaluate a prototype implementation.