BAN Logic-Based Security Proof for Mobile OTP Authentication Scheme

摘要

A Mobile One-Time Password (OTP) mechanism solves the password security problem that could result from reusing the same password multiple times. Eldefrawy et al., has presented a two-factor OTP-based authentication scheme using mobile phones which provides forward and infinite OTP generation using two nested hash functions. However, they have not formally analyzed their protocol. In this paper, we are going to formally analyze their presented algorithm with a BAN logic analysis to proof its security in a formal way. The logical postulate is applied to proof the desired attributes of our mobile OTP based two factor authentication using mobile phone. The analysis shows that the security of illustrated protocol has been formally proved.