Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols

ion for Epistemic Model Checking of Dining Cryptographers-based Protocols Omar I. Al-Bataineh and Ron van der Meyden School of Computer Science and Engineering, University of New South Wales The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. oved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents' knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and models of this protocol, and some new conclu...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Omar I. Al-Bataineh, Ron van der Meyden
• Keywords: CORR 2010, Cryptographers-based Protocols, Dining Cryptographers, Education, Epistemic Model Checking