Symbolic model checking the knowledge of the dining cryptographers
- 1 January 2004
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper describes the application of symbolic techniques (in particular, OBDDs) to model checking specifications in the logic of knowledge for an agent operating with synchronous perfect recall in an environment of which it has incomplete knowledge. It discusses the application of these techniques to the verification of a security protocol: Chaum's Dining Cryptographers protocol, which provides a mechanism for anonymous broadcastNo Full TexKeywords
This publication has 15 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Model Checking Knowledge and TimePublished by Springer Nature ,2002
- A Model Checking Algorithm for Multi-agent SystemsPublished by Springer Nature ,1999
- Common Knowledge and Update in Finite EnvironmentsInformation and Computation, 1998
- Knowledge, probability, and adversariesJournal of the ACM, 1993
- Model Checking vs. Theorem Proving: A ManifestoPublished by Elsevier ,1991
- Knowledge and common knowledge in a distributed environmentJournal of the ACM, 1990
- A logic of authenticationACM Transactions on Computer Systems, 1990
- The dining cryptographers problem: Unconditional sender and recipient untraceabilityJournal of Cryptology, 1988
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983