Title :
Symbolic model checking the knowledge of the dining cryptographers
Author :
Van der Meyden, Ron ; Suf, K.
Author_Institution :
Sch. of Comput. Sci. & Eng., Univ. of New South Wales, Australia
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 broadcast.
Keywords :
binary decision diagrams; cryptography; formal logic; formal specification; formal verification; protocols; Dining Cryptographers protocol; anonymous broadcast; knowledge logic; model checking; security protocol; symbolic techniques; Access protocols; Application software; Australia; Broadcasting; Computer science; Cryptographic protocols; Cryptography; Information analysis; Information security; Logic;
Conference_Titel :
Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE
Print_ISBN :
0-7695-2169-X
DOI :
10.1109/CSFW.2004.1310747
