Symbolic Model Checking the Knowledge of the Dining Cryptographers

This paper describes how symbolic techniques (in particular, OBDD's) may be used to to implement an algorithm for model checking specifications in the logic of knowledge for a single agent operating with synchronous perfect recall in an environment of which it has incomplete knowledge. As an illustration of the utility of this algorithm, the paper shows how it may be used to verify a security protocol: Chaum's Dining Cryptographers protocol, which provides a mechanism for anonymous broadcast. It is argued that previous approaches to model checking security protocols are unable to verify this protocol, because of its information theoretic nature.

• Type: Conference
• Year: 2004
• Where: CSFW
• Authors: Ron van der Meyden, Kaile Su
• Keywords: CSFW 2004, Model Checking, Model Checking Specifications, Security Privacy, Security Protocols