Abstract: During the past few decades deniable authentication protocol has been studied. A lot of deniable authentication protocols have been proposed which claimed that have the security properties, for example, authentication, deniability and so on. To our knowledge, these security properties and deniable authentication protocols are analyzed with informal method or with symbolic method by hand which depends on experts’ knowledge and skill and is prone to make mistakes. So analysis of security properties and deniable authentication protocols with automatic tool in symbolic model or computational model plays an important role in security protocol world and is a significant work. Especially analysis with automatic tool in computational model is a changeling issue. In this study firstly the state-of-art of deniable authentication protocol and the proof including in symbolic model and in computational model are presented. Then the term, process and correspondence assertion in Blanchet calculus is used to model security properties including deniability and deniable authentication protocols and propose the first mechanized framework of deniable authentication protocols in computational model with active adversary. The proposed mechanized framework can be used to automatically analyze the security properties including strong deniability and weak deniability of interactive or non-interactive deniable authentication protocols with CryptoVerif.