Abstract: During the past few decades a lot of deniable authentication protocols have been proposed which claimed that have the security properties, for example, deniability. To our knowledge, these security properties and deniable authentication protocols are analyzed with informal method or with symbolic method by hand which is prone to make mistakes. So analysis of security properties and deniable authentication protocols with automatic tool in symbolic model or computational model play an important role in security protocol world. Especially analysis with automatic tool in computational model is a changeling issue. Owning to the contribution of Meng and Shao, Meng non-interactive deniable authentication protocol can be analyzed with automatic tool in computational model. In this study firstly the state-of-art of deniable authentication protocol and the proof included 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 included deniability and Meng non-interactive deniable authentication protocol with Meng and Shao mechanized framework of deniable authentication protocol in computational model with active adversary. Finally Meng non-interactive deniable authentication protocol is analyzed in the computational model and Meng and Shao framework with CryptoVerif. To our knowledge, we are conducting the first automatic analysis in computational model of Meng non-interactive deniable authentication protocol. The results show that Meng non-interactive deniable authentication protocol has weak deniability and strong deniability.