Submit Manuscript

Information Technology Journal

Year: 2011 | Volume: 10 | Issue: 4 | Page No.: 717-735
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Article Trend

Total views 539

Search

Authors

Bo Meng

Keywords

Research Article

Automatic Verification of Deniable Authentication Protocol in a Probabilistic Polynomial Calculus with Cryptoverif

Bo Meng
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.
PDF Fulltext XML References Citation

Related Articles

Implementation and Evaluation of the Live-CD Based Authentication Gateway
A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model
A Secure Non-Interactive Deniable Authentication Protocol with Strong Deniability Based on Discrete Logarithm Problem and its Application on Internet Voting Protocol
Formalizing Deniability
Computationally Sound Mechanized Proofs for Deniable Authentication Protocols with a Probabilistic Polynomial Calculus in Computational Model

Leave a Comment

Your email address will not be published. Required fields are marked *