A tableaux method for dolev-yao multi-agent epistemic logic

Abstract

Given the increasing importance of security protocols in our daily lives, the efforts to develop mechanisms and models for verification of such protocols are always relevant. In this work, we propose the Dolev-Yao Multi-Agent Epistemic Logic, which is an extension of Multi-Agent Epistemic Logic, aimed to analyze security protocols and inspired by Dolev-Yao model, the seminal work in formal cryptography. We prove the soundness and completeness of our system, also demonstrating its use. Then, a tableaux method for this logic is presented, including the proofs of soundness and completeness. Finally, we provide a termination argument for our method and show some examples.