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.
Additional Metadata
THEME Null option (theme 11)
Publisher AAMAS
Conference International Workshop on Learning and Adaptation in MAS
Citation
Gattinger, M, & van Eijck, D.J.N. (2015). Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic. In Proceedings of International Workshop on Learning and Adaptation in MAS 2015 (LAMAS) (pp. 1–14). AAMAS.