Abstract

Verifying an epistemic protocol involves creating a formalized version of the protocol in a suitable logical language, and next showing (i) that the steps of the protocol are in one to one correspondence with the steps in its formalized version, (ii) that the formalized version satisfies certain correctness conditions, and (iii) hence, that the original version also satisfies these conditions. We will show that DEL is a suitable medium for carrying out this program for an interesting example protocol