Towards a Formal Verification of an Authentication Protocol Using Non-Monotonic Logic

Authentication is one of the important security properties required to identify the communicating party or to validate the received document. Several authentication techniques with many flavors have been proposed, however, most of them lack a formal security proof. In this paper, we present a two-factor authentication protocol and followed by a key establishment mechanism using only hash function. We analyze and verify the security of the proposed protocol using non-monotonic logic.