DELP: Dynamic Epistemic Logic for Security Protocols
This work addresses the problem of validating security protocols for researchers in formal methods and cryptography, but it appears incremental as it builds on existing approaches.
The paper tackles the challenge of formal analysis of security protocols by defining a complete system of dynamic epistemic logic for modeling them, and implements this logic in the theorem prover Lean to verify some of its properties.
The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.