An Omniscience-Free Temporal Logic of Knowledge for Verifying Authentication Protocols.

Since the advent of BAN logic, many logics have been proposed for verifying authentication protocols. In one line of research, scholars have presented logics that can be utilized in verifying timed requirements of the protocols. Although many temporal epistemic logics have been developed to this end, there is no complete logic of this kind to prevent logical omniscience. Thus, they may lead to misleading judgments about the properties of the protocol being analyzed. In this paper, we propose a complete and omniscience-free temporal epistemic logic for analyzing authentication protocols. The main challenging issue in devising this logic is formulating intuitive models that on one hand reflect what is naturally meant by a protocol execution and on the other hand make it possible to achieve properties such as completeness. We show that such models can build on interpreted systems and that the resulting logic is useful in analyzing authentication protocols. [ABSTRACT FROM AUTHOR]