
	Information Technology Journal
	Year: 2011 \| Volume: 10 \| Issue: 4 \| Page No.: 717-735 DOI: 10.3923/itj.2011.717.735

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

Bo Meng

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.

PDF Fulltext XML References Citation Report 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

How to cite this article:

Bo Meng , 2011. Automatic Verification of Deniable Authentication Protocol in a Probabilistic Polynomial Calculus with Cryptoverif. Information Technology Journal, 10: 717-735.

DOI: 10.3923/itj.2011.717.735

URL: https://scialert.net/abstract/?doi=itj.2011.717.735

COMMENT ON THIS PAPER

Navigation


		Online First
		Current Issue
		Previous Issues
		Editorial Board
		Submit a Manuscript
		Guide to Authors
		Subscribe to E-alerts

Indexed In


		ASCI-Database
		Asian Digital Library
		Google Scholar

Science Alert