Dynamic Epistemic Logic for Guessing Games and Cryptographic Protocols

Abstract

We present two variants of Dynamic Epistemic Logic based on a new formal representation of what it means to know a number.
The Logic of Guessing Games GG formalizes number guessing games and information updates happening in such games. We discuss many examples and provide a sound and complete axiomatization of GG.
With Epistemic Crypto Logic ECL we apply the idea of register models to the analysis of cryptographic protocols. Feasible computation and the communication between multiple agents can be expressed in the language itself, allowing for a thorough analysis in one single framework. Our main example is the famous Diffie-Hellman protocol for secret key distribution over an insecure network.
For both systems we implement model checking in Haskell. For ECL we also provide a Monte Carlo algorithm that gives probabilistic results but runs much faster than the ordinary implementation.
All source code is included as part of the text. The main features and design choices are highlighted with annotations.

Downloads

Full text: mol_thesis_gattinger_2014.pdf

Bib(La)Tex file: mol_thesis_gattinger_2014.bib

Source code: code.zip

Errata

Page 14: Definition 31 is wrong. See Definition 2.5 in [BDV01] for a correct definition of generated submodels. Thanks to Jeroen van Wier for pointing this out.

Further Links

Try it out online: Epistemic Logic Online

For the visualization of Kripke frames: KripkeVis

Modeλ Checking DEL for Guessing Games and Cryptography - Talk at the Workshop on The Logical Dynamics of Information, Agency and Interaction, ILLC, 3rd October 2014.