Subscribe Now Subscribe Today
Science Alert
 
FOLLOW US:     Facebook     Twitter
Blue
   
Curve Top
Information Technology Journal
  Year: 2011 | Volume: 10 | Issue: 4 | Page No.: 717-735
DOI: 10.3923/itj.2011.717.735
 
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail
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
 
 
 

 

 
 
 
 
 
 
 
 
 

 
 
 
 
 

       

       

Curve Bottom