Kacprzak, M.;
Lomuscio, A.;
Niewiadomski, A.;
Penczek, W.;
Raimondi, F.;
Szreter, M.;
(2006)
Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol.
Fundamenta Informaticae
, 72
(1-3)
pp. 215-234.
![[thumbnail of 5626.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
5626.pdf Download (620kB) |
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.
| Type: | Article |
|---|---|
| Title: | Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | http://fi.mimuw.edu.pl/abs72.html#15 |
| Language: | English |
| Additional information: | Special Issue on Concurrency Specification and Programming (CS&P 2005) Ruciane-Nide, Poland, 28-30 September 2005 |
| UCL classification: | |
| URI: | https://discovery.ucl.ac.uk/id/eprint/5626 |
Archive Staff Only
 |
View Item |
