首页|Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID

Formal Analysis and Improvement on Ultralightweight Mutual Authentication Protocols of RFID

扫码查看
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.

UMAPRCIARAPPKey synchronization patching schemeModel checking

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

展开 >

School of Software, East China Jiaotong University, Nanchang 330013, China

Product Development Center, CRRC ZHUZHOU LOCOMOTIVE CO., LTD, Hunan 412001, China

This work is supported by the National Natural Science Foundation of ChinaThis work is supported by the National Natural Science Foundation of ChinaNatural Science Foundation of Jiangxi ProvinceMajor Academic and Technical Leaders Foundation of Jiangxi ProvinceJiangxi Province Graduate Special Fund ProjectScience and Technology Project of Jiangxi Provincial Education Department

611630056156202620161BAB20206320172BCB22015YC2018-S261GJJ170384

2019

中国电子杂志(英文版)

中国电子杂志(英文版)

CSTPCDCSCDSCIEI
ISSN:1022-4653
年,卷(期):2019.28(5)
  • 1
  • 25