Advertisement

Verifying Randomized Byzantine Agreement_

  • Marta Kwiatkowska
  • Gethin Norman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)

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.

Keywords

Induction and compositional model checking probabilistic model checking randomized distributed algorithms. 

References

  1. 1.
    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.Google Scholar
  2. 2.
    J. Aspnes and M. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 11(3):441–460, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    C. Cachin. Distributing trust on the Internet. In Proc. DSN’01, pages 183–192. IEEE Computer Society Press, 2001.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    C. Cachin and J. Poritz. Secure intrusion-tolerant replication on the Internet. In Proc. DSN-2002, pages 167–176. IEEE Computer Society Press, 2002.Google Scholar
  7. 7.
    M. Castro and B. Liskov. Practical Byzantine fault tolerance. In Proc. ACM Symp. on Operating Systems Design and Implementation (OSDI), pages 173–186, 1999.Google Scholar
  8. 9.
    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.Google Scholar
  9. 10.
    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.Google Scholar
  10. 12.
    M. Fischer, N. Lynch, and M. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(5):374–382, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 13.
    K. Folegati and R. Segala. Coin lemmas with random variables. In Proc. PAPMPROBMIV’ 01, volume 2165 of LNCS, pages 71–86. Springer, 2001.Google Scholar
  12. 14.
    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.Google Scholar
  13. 15.
    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.Google Scholar
  14. 16.
    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.Google Scholar
  15. 17.
    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.Google Scholar
  16. 18.
    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.Google Scholar
  17. 19.
    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.Google Scholar
  18. 21.
    K. McMillan. A methodology for hardware verification using compositional model checking. Science of Computer Programming, 37(1–3):279–309, 2000.zbMATHCrossRefGoogle Scholar
  19. 22.
    K. McMillan, S. Qadeer, and J. Saxe. Induction and compositional model checking. In Proc. CAV’00, volume 1855 of LNCS, pages 312–327, 2000.Google Scholar
  20. 23.
    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.CrossRefGoogle Scholar
  21. 25.
    M. Rabin. Randomized Byzantine generals. In Proc. FOCS’83, pages 403–409. IEEE Computer Society Press, 1983.Google Scholar
  22. 26.
    A. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.Google Scholar
  23. 27.
    R. Segala. Modelling and Verifiation of Randomized Distributed Real Time Systems. PhDthesis, Massachusetts Institute of Technology, 1995.Google Scholar
  24. 28.
    R. Segala. The essence of coin lemmas. In Proc. PROBMIV’98, volume 22 of ENTCS, 1998.Google Scholar
  25. 29.
    V. Shoup. Practical threshold signatures. In Proc. Eurocrypt 2000, volume 1807 of LNCS, pages 207–220. Springer, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marta Kwiatkowska
    • 1
  • Gethin Norman
    • 1
  1. 1.School of Computer Science, University of BirminghamUK

Personalised recommendations