Submit Manuscript

Information Technology Journal

Year: 2011 | Volume: 10 | Issue: 3 | Page No.: 611-625
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Article Trend

Total views 155

Authors

Bo Meng

Fei Shao

Keywords

Research Article

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

Related Articles

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

Leave a Comment

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