  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.
