Skip to Main content Skip to Navigation
Conference papers

Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic

Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Tijs Van Der Storm Connect in order to contact the contributor
Submitted on : Monday, January 25, 2016 - 2:07:05 PM
Last modification on : Thursday, January 20, 2022 - 5:28:43 PM


  • HAL Id : hal-01261491, version 1



Malvin Gattinger, Jan Van van Eijck. Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic. Proceedings LAMAS (LAMAS 2015), 2015, Istanbul, Turkey. ⟨hal-01261491⟩



Record views