Return to search

User Efficient Authentication Protocols with Provable Security Based on Standard Reduction and Model Checking

Authentication protocols are used for two parties to authenticate each other and build a secure channel over wired or wireless public channels. However, the present standards of authentication protocols are either insufficiently secure or inefficient for light weight devices. Therefore, we propose two authentication protocols for improving the security and user efficiency
in wired and wireless environments, respectively.
Traditionally, TLS/SSL is the standard of authentication and key exchange protocols in wired Internet. It is known that the security of TLS/SSL is not enough due to all sorts of client side attacks. To amend the client side security, multi-factor authentication is an effective solution. However, this solution brings about the issue of biometric privacy which raises public concern of revealing biometric data to an authentication server. Therefore, we propose a truly three factor authentication protocol, where the authentication server can verify their biometric data without the knowledge of users¡¦ templates and samples.
In the major wireless technologies, extensible Authentication Protocol (EAP) is an authentication
framework widely used in IEEE 802.11 WLANs. Authentication mechanisms built on EAP are called EAP methods. The requirements for EAP methods in WLANs authentication have been defined in RFC 4017. To achieve user efficiency and robust security, lightweight computation and forward secrecy, excluded in RFC 4017, are desired in WLAN authentication.
However, all EAP methods and authentication protocols designed for WLANs so far do not satisfy all of the above properties. We will present a complete EAP method that utilizes stored secrets and passwords to verify users so that it can (1) meet the requirements of RFC 4017, (2) provide lightweight computation, and (3) allow for forward secrecy.
In order to prove our proposed protocols completely, we apply two different models to examine their security properties: Bellare¡¦s model, a standard reduction based on computational model, that reduces the security properties to the computationally hard problems and the OFMC/AVISPA tool, a model checking approach based on formal model, that uses the concept of the search tree to systematically find the weaknesses of a protocol. Through adopting Bellare¡¦s model and OFMC/AVISPA tool, the security of our work is firmly established.

Identiferoai:union.ndltd.org:NSYSU/oai:NSYSU:etd-0912112-040549
Date12 September 2012
CreatorsLin, Yi-Hui
ContributorsShiuh-Jeng Wang, Chun-I Fan, Chu-Hsing Lin, Chung-Huang Yang, Wen-Tsuen Chen, Wen-Shenq Juang, Chih-Hung Wang
PublisherNSYSU
Source SetsNSYSU Electronic Thesis and Dissertation Archive
LanguageEnglish
Detected LanguageEnglish
Typetext
Formatapplication/pdf
Sourcehttp://etd.lib.nsysu.edu.tw/ETD-db/ETD-search/view_etd?URN=etd-0912112-040549
Rightsunrestricted, Copyright information available at source archive

Page generated in 0.0024 seconds