Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast

TL;DR

This paper demonstrates how epistemic model checking can be used to derive and verify concrete implementations of knowledge-based protocols, exemplified through extensions of the Dining Cryptographers protocol for anonymous broadcast.

Contribution

It introduces a method to apply epistemic model checking for implementing and optimizing knowledge-based protocols based on their abstract descriptions.

Findings

Verified concrete implementations of anonymous broadcast protocols

Optimized protocols based on context-specific knowledge conditions

Extended Dining Cryptographers protocol with verified properties

Abstract

Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper 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.