Model checking of knowledge in unconditionally secure cryptographic protocols

Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The thesis describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.This thesis also provides a comprehensive introduction to epistemic logic model checking and its application to the verification of security protocols involving multiple agents. It gives the necessary background to model checking techniques. It then investigates the cause and effects of the state space explosion problem, known as the major drawback of the model checking approach. It develops ways to improve the performance of model checking for knowledge in Chaum's dining cryptographers protocol and its extensions.The thesis suggests an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved 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 is used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification