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

https://hal.inria.fr/hal-01261491
Contributor : Tijs van der Storm <>
Submitted on : Monday, January 25, 2016 - 2:07:05 PM
Last modification on : Monday, March 14, 2016 - 11:41:57 AM

Identifiers

  • HAL Id : hal-01261491, version 1

Collections

Citation

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

Share

Metrics

Record views

120