Epistemic Logic Based on Dolev-Yao Model

• Mario R. F. Benevides
• Luiz C. F. Fernandez
• Anna C. C. M. de Oliveira

DOI: https://doi.org/10.5753/etc.2017.3180

Resumo

In this work, we extend multi-agent epistemic logic for reasoning about properties in protocols. It is based on Dolev-Yao model and uses structured propositions, a new technique to deal with messages, keys and properties in security protocols in an uniform manner, keeping the logic propositional. In order to illustrate the applicability of this new logic, an example is presented. There are many approaches to formally verify authenticity and secrecy in communication protocols. In this work we are most interested in logical approaches to deal with that kind of system, in particular based on [Dolev and Yao 1983].