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.
Type de document :
Communication dans un congrès
Proceedings LAMAS (LAMAS 2015), 2015, Istanbul, Turkey. 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01261491
Contributeur : Tijs Van Der Storm <>
Soumis le : lundi 25 janvier 2016 - 14:07:05
Dernière modification le : lundi 14 mars 2016 - 11:41:57

Identifiants

  • 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. 2015. 〈hal-01261491〉

Partager

Métriques

Consultations de la notice

81