Summary: The rationale of authentication has been a topic of study for about a decade and a half. First attempts at formal analysis of authentication protocols were not using logics per se, but were certainly logical. Millen’s Interrogator was a Prolog based tool specifically designed for authentication protocol analysis that functioned essentially as a special purpose model checker. Kemmerer used the general purpose formal specification language Ina Jo and an accompanying symbolic execution tool Inatest to specify and analyze protocols.
We will focus on logics of authentication, beginning with BAN. However, we will not only be discussing logics per se. We will also be looking at the ‘rhyme and reason’ of authentication, the attempts to formalize and define notions of authentication and to apply these. Thus, we will also be considering the logic of authentication in a broader sense.
For the entire collection see [Zbl 0974.00025].