On the Properties of Epistemic and Temporal Epistemic Logics of Authentication

The authentication properties of a security protocol are specified based on the knowledge gained by the principals that exchange messages with respect to the steps of that protocol. As there are many successful attacks on authentication protocols, different formal systems, in particular epistemic and temporal epistemic logics, have been developed for analyzing such protocols. However, such logics may fail to detect some attacks. To promote the specification and verification power of these logics, researchers may try to construct them in such a way that they preserve some properties such as soundness, completeness, being omniscience-free, or expressiveness. The aim of this paper is to provide an overview of the epistemic and temporal epistemic logics which are applied in the analysis of authentication protocols to find out how far these logical properties may affect analyzing such protocols.