Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic

We present a variant of Kripke models to model knowledge of large numbers, applicable to cryptographic protocols. Our Epistemic Crypto Logic is a variant of Dynamic Epistemic Logic to describe com- munication and computation in a multi-agent setting. It is interpreted on register models which eciently encode larger Kripke models. As an example we formalize the well-known Die-Hellman key exchange. The presented register models also motivate a Monte Carlo method for model checking which we compare against a standard algorithm, using the key exchange as a benchmark.