Abstract: The peer entity authentication is an important service in the network security architecture. This paper introduces an authentication protocol with time stamp in a computer network environment, which treats a sender and a receiver symmetrically and makes no assumption about any specific time ordering of events. Based on the state transition directed graph of the protocol,this paper verifies the important properties of the protocol, including completeness, deadlock freeness, livelock freeness, termination, boundedness, and absence of non-executable interactions, by applying a reachability analysis.