Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID

XIAO Meihua; LI Wei; ZHONG Xiaomei; YANG Ke; CHEN Jia

doi:10.1049/cje.2019.06.022

Volume 28 Issue 5

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2019 > 28(5): 1025-1032

XIAO Meihua, LI Wei, ZHONG Xiaomei, et al., “Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID,” Chinese Journal of Electronics, vol. 28, no. 5, pp. 1025-1032, 2019, doi: 10.1049/cje.2019.06.022

Citation:

XIAO Meihua, LI Wei, ZHONG Xiaomei, et al., “Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID,” Chinese Journal of Electronics, vol. 28, no. 5, pp. 1025-1032, 2019, doi: 10.1049/cje.2019.06.022

Citation:

PDF( 1733 KB)

Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID

doi: 10.1049/cje.2019.06.022

1.
School of Software, East China Jiaotong University, Nanchang 330013, China;
2.
Product Development Center, CRRC ZHUZHOU LOCOMOTIVE CO., LTD, Hunan 412001, China

Funds: This work is supported by the National Natural Science Foundation of China (No.61163005, No.61562026), the Natural Science Foundation of Jiangxi Province (No.20161BAB202063), the Major Academic and Technical Leaders Foundation of Jiangxi Province (No.20172BCB22015), the Jiangxi Province Graduate Special Fund Project (No.YC2018-S261), and the Science and Technology Project of Jiangxi Provincial Education Department(No.GJJ170384)

More Information

Corresponding author: LI Wei (corresponding author) was born in 1992.He gained master degree from East China Jiaotong University.Now he serves as a researcher at CRRC Zhuzhou Locomotive Co,Ltd.His research interests include Information Security,Software Formal Method.(Email:vic.me@foxmail.com)
Received Date: 2018-06-06
Rev Recd Date: 2018-11-13
Publish Date: 2019-09-10

Abstract

Abstract

Ultralightweight mutual authentication protocols (UMAP) of Radio frequency identification (RFID) systems have attracted much attention from researchers. Many studies reveal that most of UMAP suffer malicious attack. To improve security of UMAP, formal analysis is performed with Simple promela interpreter (SPIN). Two typical UMAPs, which are RCIA and RAPP, are selected as our case study. A protocol abstract modeling method is presented to make UMAP can be formalized simply. Using SPIN, verification results show that RCIA and RAPP are both vulnerable against desynchronization attack. A Generalized model of UMAP (G-UMAP) and a general patching scheme are presented for resisting the attack. To validate the patching scheme, formal verification is then performed for the improved protocol. SPIN verification shows that the improved RCIA and RAPP both gain higher security. The above proposed modeling method has great significance for similar UMAP analyzing, and the proposed patching scheme is proved to be practical and reliable.
- UMAP,
- RCIA,
- RAPP,
- Key synchronization patching scheme,
- Model checking

FullText(HTML)

References(25)

References

NLi, Shancang, Theo Tryfonas, and Honglei Li, "The Internet of Things:a security point of view", Internet Research, Vol.26, No.2 pp.337-359, 2016

López P.P., "Lightweight cryptography in radio frequency identification (RFID) systems", Ph.D. dissertation, Computer Science Department, Carlos Ⅲ University of Madrid, 2008.

Ahmadian, Zahra, Mahmoud Salmasizadeh, and Mohammad Reza Aref, "Desynchronization attack on RAPP ultralightweight authentication protocol", Information processing letters, Vol.113, No.7, pp.205-209, 2013.

Peris-Lopez, Pedro, et al., "LMAP:A real lightweight mutual authentication protocol for low-cost RFID tags", in Proc. of 2nd Workshop on RFID Security, Vol.2006, No.06, pp.100-112.

Chien, Hung-Yu, "SASI:A new ultralightweight RFID authentication protocol providing strong authentication and strong integrity", IEEE transactions on dependable and secure computing, Vol.4, No.4, pp.337-340,2007

Peris-Lopez, Pedro, et al., "Advances in ultralightweight cryptography for low-cost RFID tags:gossamer protocol", In-ternational Workshop on Information Security Applications. Springer, Berlin, Heidelberg, pp.56-68, 2008.

Tian, Y., Chen, G., Li J., "A new ultralightweight RFID authentication protocol with permutation", IEEE Communications Letters, Vol.16, No.5, pp.702-705, 2012.

Zhuang X, Zhu Y, Chang C C., "A new ultralightweight RFID protocol for low-cost tags:R2AP", Wireless Personal Communications, Vol.79, No.3, pp.1787-1802,2014.

Mujahid U, Najam-Ul-Islam M, Shami M.A., "RCIA:A new ultralightweight RFID authentication protocol using recursive hash", International Journal of Distributed Sensor Networks, Vol.11, No.1, pp.1-8, 2015.

Mujahid U, Najam-ul-Islam M, Sarwar S., "A new ultralightweight RFID authentication protocol for passive low cost tags:KMAP", Wireless Personal Communications, Vol.94, No.3, pp.725-744, 2017.

Mujahid U, Najam-ul-Islam M, Qurat-Ul-Ain R.A, et al., "Cryptanalysis of two ultralight-weight mutual authentication protocols", Science International (Lahore), Vol.28, No.6, pp.5079-5086, 2016.

Bilal Z,Martin K, Saeed Q., "Multiple attacks on authentication protocols for low-cost RFID tags", Applied Mathematics & Information Sciences, Vol.9, No.2, pp.561-570, 2015.

Barrero D F, Hernández-Castro J C, Peris-Lopez P, et al., "A genetic tango attack against the David-Prasad RFID ultralightweight authentication protocol", Expert Systems, Vol.31, No.1, pp.9-19, 2014.

Xiao Meihua, Cheng Daolei, Li Wei, et al., "Formal analysis and verification of OAuth 2.0 protocol improved by key cryptosystems", Chinese Journal of Electronics, Vol.26, No.3, pp.477-484, 2017.

Xiao M, Ma C, Deng C, et al., "A novel approach to automatic security protocol analysis based on authentication event logic", Chinese Journal of Electronics, Vol. 24, No.1, pp.187-192, 2015.

Holzmann, G.J., "The model checker SPIN", IEEE Transactions on Software Engineering, Vol.23, No.5, pp.279-295, 1997.

Ahmadian Z, Salmasizadeh M, Aref M R., "Recursive linear and differential cryptanalysis of ultralightweight authentication protocols", IEEE Transactions on Information Forensics and Security, Vol.8, No.7, pp.1140-1151, 2013.

Bruce, N., Kim, H., Kang, Y., Lee, Y., Lee, H., "On modeling protocol-based clustering tag in RFID systems with formal security analysis", 2015 IEEE 29th International Conference on Advanced Information Networking and Applications (AINA), 2015, pp.498-505.

Qingling C, Yiju Z, Yonghua W., "A minimalist mutual authentication protocol for RFID system & BAN logic analysis", Computing Communication Control and Management ISECS International Colloquium on IEEE, No.2, pp.449-453, 2008.

Li J, Zhou Z, Wang P., "Cryptanalysis of the LMAP protocol:A low-cost RFID authentication protocol", 201729th Chinese Control And Decision Conference (CCDC), Chongqing, 2017, pp.7292-7297.

Islam, S., "Security analysis of LMAP using AVISPA", International Journal of Security and Networks, Vol.9, No.1, pp.30-39, 2014.

Guanjie Yuan and Shigong Long, "Formal verification of RFID protocols using nuXmv", 201610th IEEE International Conference on Anticounterfeiting Security and Identification (ASID), Xiamen, 2016, pp.58-62.

Maggi, Paolo, and Riccardo Sisto, "Using SPIN to verify security properties of cryptographic protocols". International SPIN Workshop on Model Checking of Software. Springer, Berlin, Heidelberg, pp.187-204, 2002.

Li W, Xiao M, Li Y, et al., "Formal Analysis and Verification for an Ultralightweight Authentication Protocol RAPP of RFID", National Conference of Theoretical Computer Science. Springer, Singapore, 2017, pp.119-132

XIAO Meihua, JIANG Yun and LIU Qiaowei, "On formal analysis of cryptographic protocols and supporting tool". Chinese Journal of Electronics, Vol.19, No.2, pp.223-228, 2010.

Relative Articles

Supplements(0)

Cited By

Proportional views