To know or not to know: epistemic approaches to security protocol verification

Security properties naturally combine temporal aspects of protocols with aspects of knowledge of the agents. Since BAN-logic, there have been several initiatives and attempts to incorporate epistemics into the analysis of security protocols. In this paper, we give an overview of work in the field and present it in a unified perspective, with comparisons on technical subtleties that have been employed in different approaches. Also, we study to which degree the use of epistemics is essential for the analysis of security protocols. We look for formal conditions under which knowledge modalities can bring extra expressive power to pure temporal languages. On the other hand, we discuss the cost of the epistemic operators in terms of model checking complexity.History & Philosophy Of SciencePhilosophyA&HCISCI(E)SSCI2ARTICLE51-7617