A quantifier-free first-order knowledge logic of authentication

In this paper we introduce a new, complete and decidable knowledge logic of authentication with a well defined semantics, intended for model checking verification of properties of authentication protocols. It is a version of the old BAN logic but with no belief modality, no modality at all, and with clearly expressible knowledge predicate. The new logic enjoys carefully defined and developed knowledge sets of the participants, with a potential intruder's knowledge and a well defined algorithm of gaining, extracting and generating knowledge. The semantics is provided with a computation structure modelling a considered authentication protocol as a transition system. We provide a sound and complete axiomatization of the new logic and prove its decidability. From a pure mathematical logic standpoint, the new logic is a simple quantifier-free first order extension of the classical propositional calculus, while it is not a typical logic of knowledge, nor is it an extension of the BAN-logic. As the correctness property of an authentication protocol we require that the agents identify themselves by showing that they know the right keys.