Toward dynamic epistemic verification of zero-knowledge protocols

We outline a novel approach for formally verifying zero-knowledge protocols building on Dynamic Epistemic Logic (DEL) as an abstract semantics for a low-level protocol specification language called SPEC. One of the main benefits is that our methodology abstracts the logical structure of the interactions from the mathematical subtleties related to cryptographic primitives. Furthermore, we leverage the DEL action structures to verify the knowledge dynamics generated by the protocol runs. We illustrate our methodology by applying it to a new protocol called BKP, and we prove that it meets the participants’ goals.