Subscribe Now Subscribe Today
Science Alert
Curve Top
Information Technology Journal
  Year: 2011 | Volume: 10 | Issue: 3 | Page No.: 611-625
DOI: 10.3923/itj.2011.611.625
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Computationally Sound Mechanized Proofs for Deniable Authentication Protocols with a Probabilistic Polynomial Calculus in Computational Model

Bo Meng and Fei Shao

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.
PDF Fulltext XML References Citation Report Citation
  •    Automatic Verification of Security Properties of OAuth 2.0 Protocol with Cryptoverif in Computational Model
  •    Automatic Verification of Deniable Authentication Protocol in a Probabilistic Polynomial Calculus with Cryptoverif
  •    Impact of Data Privacy and Confidentiality on Developing Telemedicine Applications: A Review Participates Opinion and Expert Concerns
  •    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
How to cite this article:

Bo Meng and Fei Shao, 2011. Computationally Sound Mechanized Proofs for Deniable Authentication Protocols with a Probabilistic Polynomial Calculus in Computational Model. Information Technology Journal, 10: 611-625.

DOI: 10.3923/itj.2011.611.625






Curve Bottom