Affiliations: Institute of Mathematics and Computer Science, Jan
Długosz University Armii Krajowej 13/15, 42-200 Cz�stochowa,
Poland. E-mail: [email protected] | Institute of Computer Science, Polish Academy of
Sciences Ordona 21, 01-237 Warsaw, Poland and Kielce University of Commerce
Peryferyjna 15, 25-562 Kielce, Poland. E-mail: [email protected]
Abstract: 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.
