Abstract
Authentication protocols are used to ensure the identity of a participant in a distributed environment. Since designing authentication protocols is an error prone process, formal verification techniques are used to verify the correctness of authentication protocols. In this paper, we develop simple but rigorous logic-based tests for the analysis of authentication protocols. In particular, we extend the framework of Distributed Temporal Protocol Logic (DTPL), and provide authentication tests at a higher level of abstraction. These tests can be easily applied on a variety of authentication protocols, yet they are rigorous enough to capture full capabilities of a typical Dolev-Yao intruder.