Sciweavers

Share
CSFW
2004
IEEE

Symbolic Model Checking the Knowledge of the Dining Cryptographers

12 years 1 months ago
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.
Ron van der Meyden, Kaile Su
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CSFW
Authors Ron van der Meyden, Kaile Su
Comments (0)
books