We propose a dynamic epistemic framework for the verification of security protocols. First, we introduce a dynamic epistemic logic equipped with iteration and cryptographic supplements in which we can formalize and check (epistemic) requirements of security protocols. On top of this, we give a general guide how to go from a protocol specification to its representation in our framework. We demonstrate this by checking requirements of a simplified version of a protocol for confidential message comparison.
Logics of knowledge and belief (including belief change) (msc 03B42)
Software (theme 1)
King’s College Publications
J. F. A. K. van Benthem (Johan) , S. Ju (Shier) , F. Veltman
Verification and Epistemics of Multi-Party Protocol Security (is een SEN1 en SEN2 project)
Logic, Rationality and Interaction
Software Analysis and Transformation

Dechesne, F, & Wang, Y. (2007). Dynamic epistemic verification of security protocols: framework and case study. In J. F. A. K van Benthem, S Ju, & F Veltman (Eds.), A Meeting of the Minds–Proceedings of the Workshop on Logic, Rationality and Interaction (pp. 129–144). King’s College Publications.