Volume 31 Issue 1
Jan.  2022
Turn off MathJax
Article Contents
ZHONG Xiaomei, XIAO Meihua, ZHANG Tong, YANG Ke, LUO Yunxian. Proving Mutual Authentication Property of RCIA Protocol in RFID Based on Logic of Events[J]. Chinese Journal of Electronics, 2022, 31(1): 79-88. doi: 10.1049/cje.2021.00.101
Citation: ZHONG Xiaomei, XIAO Meihua, ZHANG Tong, YANG Ke, LUO Yunxian. Proving Mutual Authentication Property of RCIA Protocol in RFID Based on Logic of Events[J]. Chinese Journal of Electronics, 2022, 31(1): 79-88. doi: 10.1049/cje.2021.00.101

Proving Mutual Authentication Property of RCIA Protocol in RFID Based on Logic of Events

doi: 10.1049/cje.2021.00.101
Funds:  This work was supported by the National Natural Science Foundation of China (61962020, 61562026)
More Information
  • Author Bio:

    was born in 1980, she is a Ph.D. candidate at school of software, East China Jiaotong University. Her research interests include information security and formal method. (Email: zhongxm@ecjtu.edu.cn)

    (corresponding author) was born in 1967, CCF Member. He is a Professor and Ph.D. Supervisor at School of Software, East China Jiaotong University, CCF Senior Member. His research interests include information security and formal method. (Email: xiaomh@ecjtu.edu.cn)

    was born in 1996, She is a master candidate at School of Software, East China Jiaotong University. Her research interests include information security and formal method. (Email: zt422zt@163.com)

    was born in 1993, he is a Ph.D. candidate at School of Software, East China Jiaotong University. His research interests include information security and formal method. (Email: landexplorer@163.com)

    was born 1998, he is a master candidate at School of Software, East China Jiaotong University. His research interests include information security and formal method. (Email: shinra2020@163.com)

  • Received Date: 2021-03-24
  • Accepted Date: 2021-06-25
  • Available Online: 2021-09-24
  • Publish Date: 2022-01-05
  • The increasing commercialization and massive deployment of radio frequency identification (RFID) systems has raised many security related issues which in return evokes the need of security protocols. Logic of events theory (LoET) is a formal method for constructing and reasoning about distributed systems and protocols that involve concepts of security. We propose fresh ciphertext and ciphertext release lemmas to extend LoET for analyzing and proving the security of authentication protocols that use symmetric key cryptography more than just digital signature. Based on the extended LoET we formally analyze and prove the authentication property of RCIA protocol, which provides mutual authentication between Tag and Reader in RFID system. Our proof approach based on extended LoET could be applied to the design and analysis of such ultralightweight RFID mutual authentication protocols.
  • loading
  • [1]
    U. Mujahid, M. Najam-ul-Islam, and M. Shami, “RCIA: A new ultralightweight RFID authentication protocol using recursive hash,” International Journal of Distributed Sensor Networks, vol.2015, no.3, pp.1–8, 2015.
    [2]
    Z. Bilal and K. Martin, “Ultra-lightweight mutual authentication protocols: Weaknesses and countermeasures,”in Proc. of 2013 Int. Conf. on Availability, Reliability and Security, NW Washington, DC, pp.304–309, 2013.
    [3]
    A. Datta, A. Derek, J. C. Mitchell, et al., “Protocol composition logic (PCL),” Electronic Notes in Theoretical Computer Science, vol.172, pp.311–358, 2007. doi: 10.1016/j.entcs.2007.02.012
    [4]
    J. Wang, N. Zhan, X. Feng, et al., “Overview of formal methods,” Journal of Software, vol.30, no.1, pp.33–61, 2019. (in Chinese)
    [5]
    W. D. Li, G. O. Passmore, and L. C. Paulson, “Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL,” Journal of Automated Reasoning, vol.62, no.1, pp.69–91, 2019.
    [6]
    W. D. Li and L. C. Paulson, “Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL,” Journal of Automated Reasoning, vol.64, no.2, pp.331–360, 2020. doi: 10.1007/s10817-019-09521-3
    [7]
    J. Divasón, S. Joosten, O. Kunar, et al., “Efficient certification of complexity proofs: Formalizing the Perron-Frobenius theorem (invited talk paper),” in Proc. of the 7th ACM SIGPLAN International Conference, New York, NY, DOI: 10.1145/3176245.3167103, 2018.
    [8]
    A. Bentkamp, J. C. Blanchette, and D. Klakow, “A formal proof of the expressiveness of deep learning,” Journal of Automated Reasoning, vol.63, no.2, pp.347–368, 2019. doi: 10.1007/s10817-018-9481-5
    [9]
    H. Barbosa, J. C. Blanchette, M. Fleury, et al., “Scalable fine-grained proofs for formula processing,” Journal of Automated Reasoning, vol.64, no.3, pp.485–510, 2020. doi: 10.1007/s10817-018-09502-y
    [10]
    ZHU Jian, HU Kai, and ZHANG Bojun, “Review on formal verification of smart contract,” Acta Electronica Sinica, vol.49, no.4, pp.792–804, 2021.
    [11]
    M. Bickford, “Component specification using event classes,” in Proc. of 12th International Symposium on Component-Based Software Engineering, East Stroudsburg, PA, pp.140−155, 2009.
    [12]
    M. Bickford, “Automated proof of authentication protocols in a logic of events,” in Proc. of the 6th International Verification Workshop, Toronto, pp.13–30, 2008.
    [13]
    M. Xiao and M. Bickford, “Logic of events for proving security properties of protocols,” in Proc. of International Conference on Web Information Systems and Mining, Shanghai, pp.519–523, 2009.
    [14]
    H. Y. Chien, T. C. Wu, and M. K. Yeh, “Provably secure gateway-oriented password-based authenticated key exchange protocol resistant to password Guessing attacks,” Journal of Information Science and Engineering, vol.29, pp.249–265, 2013.
    [15]
    K. Yang, M. H. Xiao, J. W. Song, et al., “Proving mutual authentication property of KerNeeS protocol based on logic of events,” IEEE Access, vol.6, pp.51853–51863, 2018. doi: 10.1109/ACCESS.2018.2870200
    [16]
    M. H. Xiao, C. L. Ma, C. Y. Deng, 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. doi: 10.1049/cje.2015.01.031
    [17]
    J. W. Song, M. H. Xiao, K. Yang, et al., “LoET-E: A refined theory for proving security properties of cryptographic protocols,” IEEE Access, vol.7, pp.59871–59883, 2019. doi: 10.1109/ACCESS.2019.2915645
    [18]
    P. Peris-Lopez, J. Hernandez-Castro, J. Tapiador, et al., “LMAP: A real lightweight mutual authentication protocol for low-cost RFID tags,” in Proc. of 2nd Workshop on RFID Security, pp.100–112, 2006.
    [19]
    P. Peris-Lopez, J. C. H. Castro, J. M. Estévez-Tapiador, et al., “EMAP: An efficient mutual-authentication protocol for low-cost RFID tags,” in Proc. of OTM Confederated International Conference “On the Move to Meaningful Internet Systems”: OTM 2006 Workshops, Montpellier, pp.352−361, 2006.
    [20]
    Y. Tian, G. Chen, and J. Li, “A new ultralightweight RFID authentication protocol with permutation,” IEEE Communications Letters, vol.16, no.5, pp.702–705, 2012. doi: 10.1109/LCOMM.2012.031212.120237
    [21]
    H. Y. Chien, “SASI: A new ultralightweight RFID authentication protocol providing strong authentication and strong integrity,” IEEE Transactions on Dependable Secure Computing, vol.4, no.4, pp.337–340, 2007. doi: 10.1109/TDSC.2007.70226
    [22]
    H. M. Sun, W. C. Ting, and K. H. Wang, “On the security of Chien’s ultralightweight RFID authentication protocol,” IEEE Trans. on Dependable Secure Computing, vol.8, no.2, pp.315–317, 2011. doi: 10.1109/TDSC.2009.26
    [23]
    G. Avoine, X. Carpent, and B. Martin, “Privacy-friendly synchronized ultralightweight authentication protocols in the storm,” Journal of Network Computer Applications, vol.35, no.2, pp.826–843, 2012. doi: 10.1016/j.jnca.2011.12.001
    [24]
    Z. Ahmadian, M. Salmasizadeh, and M. R. Aref, “Desynchronization attack on RAPP ultralightweight authentication protocol,” Information Processing Letters, vol.113, no.7, pp.205–209, 2013. doi: 10.1016/j.ipl.2013.01.003
    [25]
    D. F. Barrero, J. C. Hernández-Castro, P. Peris-Lopez, et al., “A genetic tango attack against the David–Prasad RFID ultra‐lightweight authentication protocol,” Expert Systems, vol.31, no.1, pp.9–19, 2014. doi: 10.1111/j.1468-0394.2012.00652.x
    [26]
    Q. U. Ain, Y. Mahmood, U. Mujahid, et al., “Cryptanalysis of mutual ultralightweight authentication protocols: SASI & RAPP,” in Proc. of 2014 International Conference on Open Source Systems and Technologies, Lahore, pp.136–145, 2015.
    [27]
    Z. Bilal, K. Martin, and Q. Saeed, “Multiple attacks on authentication protocols for low-cost RFID tags,” Applied Mathematics & Information Sciences, vol.9, no.2, pp.561–569, 2015.
    [28]
    ZHANG Qikun, WANG Bingli, ZHANG Xiaosong, et al., “Blockchain-based dynamic group key agreement protocol for Ad Hoc network,” Chinese Journal of Electronics, vol.29, no.3, pp.447–454, 2020. doi: 10.1049/cje.2020.02.020
    [29]
    Muhammad Naeem, Shehzad Ashraf Chaudhry, Khalid Mahmood, et al., “A scalable and secure RFID mutual authentication protocol using ECC for Internet of things,” International Journal of Communication Systems, vol.33, no.13, DOI: 10.1002/dac.3906, 2020.
    [30]
    Q. Qian, Y. L. Jia, and R. Zhang, “A lightweight RFID security protocol based on elliptic curve cryptography,” Network Security, vol.18, pp.354–361, 2016.
    [31]
    C. Qingling, Z. Yiju, and W. Yonghua, “A minimalist mutual authentication protocol for RFID system & BAN logic analysis,” in Proc. of ISECS International Colloquium on Computing, Communication, Control, & Management, IEEE, Guangzhou, pp.449−453, 2008.
    [32]
    J. Li, Z. Zhou, and P. Wang, “Cryptanalysis of the LMAP protocol: A low-cost RFID authentication protocol,” in Proc. of 29th Chinese Control and Decision Conference (CCDC), Chongqing, DOI: 10.1109/CCDC.2017.7978502, 2017.
    [33]
    X. Zhuang, Y. Zhu, and C. C. Chang, “A new ultralightweight RFID protocol for low-cost tags: R2AP,” Wireless Personal Communications, vol.79, no.3, pp.1787–1802, 2014. doi: 10.1007/s11277-014-1958-x
    [34]
    X. Zhong, M. Xiao, W. Li, J. Chen, et al., “Formal analysis and improvement of RCIA: An ultra-lightweight RFID mutual authentication protocol,” Computer Engineering and Science, vol.40, pp.2183–2192, 2018. (in Chinese)
    [35]
    M. H. Xiao, W. Li, X. M. Zhong, 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
    [36]
    M. Bickford, “Unguessable atoms: A logical foundation for security,” in Proc. of the Second International Conference on Verified Software: Theories, Tools, Experiments, Toronto, pp.30−53, 2008.
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(4)  / Tables(1)

    Article Metrics

    Article views (226) PDF downloads(23) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return