DocumentCode
3129493
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
fYear
2004
fDate
28-30 June 2004
Firstpage
280
Lastpage
291
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE
ISSN
1063-6900
Print_ISBN
0-7695-2169-X
Type
conf
DOI
10.1109/CSFW.2004.1310747
Filename
1310747
Link To Document