Dynamic epistemic verification of security protocols: framework and case study
Presented at the Logic, Rationality and Interaction, Beijing
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|
|Organisation||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.