Abstract: A formal framework of deniability in the deniable authentication protocol is presented. By introducing Kessler and Neumann logic as a tool, the proposed framework formalizes the strong deniability and weak deniability, which are the key properties in the deniable authentication protocol. The formal framework establishes what can construct an evidence of deniability. Based on the construction, the simple and easy to be applied framework enables the identification of deniability and provides a heuristic to take evidence of deniability into consideration in the early stages of designing a deniable authentication protocol. Two typical deniable authentication protocols, including a interactive and a non-interactive one are analyzed by both informal method and the proposed formal framework.