Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol

Issue title: SPECIAL ISSUE ON CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P 2005) Ruciane-Nide, Poland, 28–30 September 2005

Article type: Research Article

Authors: Kacprzak, Magdalena | Lomuscio, Alessio | Niewiadomski, Artur | Penczek, Wojciech | Raimondi, Franco | Szreter, Maciej

Affiliations: Białystok University of Technology, PL. E-mail: mdkacprzak@wp.pl | University College London, UK. E-mail: a.lomuscio@cs.ucl.ac.uk | Podlasie Academy, PL. E-mail: artur@iis.ap.siedlce.pl | Institute of Computer Science, PAS, and Podlasie Academy, PL. E-mail: penczek@ipipan.waw.pl | Institute of Computer Science, PAS, PL. E-mail: mszreter@ipipan.waw.pl

Abstract: We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.

Keywords: verification, Dining Cryptographers Protocol, bounded model checking, binary decision diagrams, SAT-solver

Journal: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 215-234, 2006