Subscribe Now Subscribe Today
Science Alert
 
Blue
   
Curve Top
Information Technology Journal
  Year: 2013 | Volume: 12 | Issue: 12 | Page No.: 2273-2285
DOI: 10.3923/itj.2013.2273.2285
 
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Automatic Verification of Security Properties of OAuth 2.0 Protocol with Cryptoverif in Computational Model

Xingdong Xu, Leyuan Niu and Bo Meng

Abstract:
During the past several years, OAuth 2.0 protocol has been widely implemented and deployed. In order to give a strong confidence in its security to the people, in this study, Blanchet calculus in computational model is used to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif. The term, process and correspondence are used to model OAuth 2.0 protocol . The authentication is formalized by non-injective or injective correspondence. The results show that OAuth 2.0 protocol has not authentication between the resource owner and authorization server, authentication between client and authorization server. The first automatic analysis on OAuth 2.0 protocol in computational model of in active adversary is implemented in this study.
PDF Fulltext XML References Citation Report Citation
 RELATED ARTICLES:
  •    Computationally Sound Mechanized Proofs for Deniable Authentication Protocols with a Probabilistic Polynomial Calculus in Computational Model
  •    A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model
How to cite this article:

Xingdong Xu, Leyuan Niu and Bo Meng, 2013. Automatic Verification of Security Properties of OAuth 2.0 Protocol with Cryptoverif in Computational Model. Information Technology Journal, 12: 2273-2285.

DOI: 10.3923/itj.2013.2273.2285

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

COMMENT ON THIS PAPER
 
 
 

 

 
 
 
 
 
 
 
 
 

 
 
 
 
 

Curve Bottom