Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic
Presented at the International Workshop on Learning and Adaptation in MAS, Istanbul, Turkey
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.
|International Workshop on Learning and Adaptation in MAS|
|Organisation||Software Analysis and Transformation|
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.