Abstract
Distributed systems increasingly rely on fault-tolerant and secure authorization services. An essential primitive used to implement such services is the Byzantine agreement protocol for achieving agreement among n parties even if t parties (t < n/3) are corrupt and behave maliciously. We describe our experience verifying the randomized protocol ABBA (Asynchronous Binary Byzantine Agreement) of Cachin, Kursawe and Shoup [5], a practical protocol that incorporates modern threshold-cryptographic techniques and forms a core of powerful asynchronous broadcast protocols [4]. The protocol is efficient (runs in constant expected time), optimal (it tolerates the maximum number of corrupted parties) and provably secure (in the random oracle model). We model the protocol in Cadence SMV, replacing the coin tosses with nondeterministic choice, and provide a proof of the protocol correctness for all n under the assumption that the cryptographic primitives are correct. The proof is fully automated except for one high-level inductive argument involving probabilistic reasoning. We validate probabilistic reasoning through deriving abstractions for finite configurations (for n up to 20) and model checking those with the probabilistic model checker PRISM.
Supported in part by EPSRC grants GR/M04617 and GR/N22960.
Contact author. Tel: +44 121 414-4789, fax: +44 121 414-4281.
Chapter PDF
Similar content being viewed by others
Keywords
References
P. Abdulla, C. Baier, P. Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. CONCUR’00, volume 1877 of LNCS, pages 320–333. Springer, 2000.
J. Aspnes and M. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 11(3):441–460, 1990.
C. Cachin. Distributing trust on the Internet. In Proc. DSN’01, pages 183–192. IEEE Computer Society Press, 2001.
C. Cachin, K. Kursawe, F. Petzold, and V. Shoup. Secure and efficient asynchronous broadcast protocols (extended abstract). In Proc. CRYPTO 2001, volume 2139 of LNCS, pages 524–541. Springer, 2001.
C. Cachin, K. Kursawe, and V. Shoup. Random oracles in Constantinople: practical asynchronous Byzantine agreement using cryptography (extended abstract). In Proc. PODC’00, pages 123–132. ACM Press, 2000.
C. Cachin and J. Poritz. Secure intrusion-tolerant replication on the Internet. In Proc. DSN-2002, pages 167–176. IEEE Computer Society Press, 2002.
M. Castro and B. Liskov. Practical Byzantine fault tolerance. In Proc. ACM Symp. on Operating Systems Design and Implementation (OSDI), pages 173–186, 1999.
P. D’Argenio, B. Jeannet, H. Jensen, and K. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Proc. PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 39–56. Springer, 2001.
L. de Alfaro, T. Henzinger, and R. Jhala. Compositional methods for probabilistic systems. In Proc. CONCUR’01, volume 2154 of LNCS, pages 351–365. Springer, 2001.
M. Fischer, N. Lynch, and M. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(5):374–382, 1985.
K. Folegati and R. Segala. Coin lemmas with random variables. In Proc. PAPMPROBMIV’ 01, volume 2165 of LNCS, pages 71–86. Springer, 2001.
J. Hurd. Verification of the Miller-Rabin probabilistic primality test. In Proc. TPHOLs’01, number EDI-INF-RR-0046 in Informatics Report Series, pages 223–238. Division of Informatics, University of Edinburgh, 2001.
M. Kwiatkowska and G. Norman. Automated verification of a randomized Byzantine agreement protocol. Technical Report CSR-01-11, University of Birmingham, School of Computer Science, 2001.
M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS’02, volume 2280 of LNCS, pages 52–67. Springer, 2002.
M. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus algorithm using Cadence SMV and PRISM. In Proc. CAV’01, volume 2102 of LNCS, pages 194–206. Springer, 2001.
M. Kwiatkowska, G. Norman, and J. Sproston. Symbolic computation of maximal probabilistic reachability. In Proc. CONCUR’01, volume 2154 of LNCS, pages 169–183. Springer, 2001.
M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE1394 Firewire root contention. Special Issue of Formal Aspects of Computing, 2002. To appear.
K. McMillan. A methodology for hardware verification using compositional model checking. Science of Computer Programming, 37(1–3):279–309, 2000.
K. McMillan, S. Qadeer, and J. Saxe. Induction and compositional model checking. In Proc. CAV’00, volume 1855 of LNCS, pages 312–327, 2000.
A. Pogosyants, R. Segala, and N. Lynch. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing, 13(3):155–186, 2000.
M. Rabin. Randomized Byzantine generals. In Proc. FOCS’83, pages 403–409. IEEE Computer Society Press, 1983.
A. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.
R. Segala. Modelling and Verifiation of Randomized Distributed Real Time Systems. PhDthesis, Massachusetts Institute of Technology, 1995.
R. Segala. The essence of coin lemmas. In Proc. PROBMIV’98, volume 22 of ENTCS, 1998.
V. Shoup. Practical threshold signatures. In Proc. Eurocrypt 2000, volume 1807 of LNCS, pages 207–220. Springer, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kwiatkowska, M., Norman, G. (2002). Verifying Randomized Byzantine Agreement_. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_13
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive