Formal analysis of PUFs-based authentication protocols in logic of events theory

被引：0
|
作者：
Zhong X. [1 ]
Xiao M. [1 ]
Yang K. [1 ]
Luo Y. [1 ]
机构：
[1] School of Software, East China Jiaotong University, Nanchang
来源：
Huazhong Keji Daxue Xuebao (Ziran Kexue Ban)/Journal of Huazhong University of Science and Technology (Natural Science Edition) | 2024年 / 52卷 / 02期
关键词：
formal methods; logic of events theory (LoET); mutual authentication protocol; physical unclonable functions (PUFs); theorem proving;
D O I：
10.13245/j.hust.240209
中图分类号：
学科分类号：
摘要：
Two novel event temporal concepts and related rules were proposed，which were used to analyze temporal order of events associated with nonces．Random session key generation of physical unclonable functions (PUFs) was formally abstracted and logic of events theory (LoET) was extended to formally analyze the PUFs-based security protocols．Taking the analysis of a SRAM (static random access memory) PUFs-based protocol as an example，the process of the random key generation and mutual authentication were formally specified，and the extended LoET was used to prove that the protocol satisfies mutual strong authentication under reasonable assumptions with theorem proving．The study shows that the extended LoET can be used to design and analyze PUFs-based security protocols． © 2024 Huazhong University of Science and Technology. All rights reserved.
引用
收藏
页码：69 / 76
页数：7
相关论文
共 20 条
  • [1] PAPPU R，, RECHT B, Physical one-way functions[J], Science, 297, 5589, pp. 2026-2030, (2002)
  • [2] O'Neill M．, Insecurity by design：today's IoT device security problem[J], Engineering, 2, 1, pp. 48-49, (2016)
  • [3] CHATTERJEE U，, CHAKRABORTY R S，, MUKHOPADHYAY D．, A PUF-based secure communication protocol for IoT[J], ACM Transactions on Embedded Computing Systems, 16, 3, pp. 1-25, (2017)
  • [4] SUH G E，, DEVADAS S．, Physical unclonable functions for device authentication and secret key generation[C], Proc of the 44th annual Design Automation Conference, pp. 9-14, (2007)
  • [5] DELVAUX J, GU D, SCHELLEKENS D, Secure lightweight entity authentication with strong PUFs：mission impossible?[C], Proc of International Workshop on Cryptographic Hardware & Embedded Systems, pp. 451-475, (2014)
  • [6] ARMKNECHT F, SADEGHI A, A formalization of the security features of physical functions[C], Proc of 2011 IEEE Symposium on Security and Privacy, pp. 397-412, (2011)
  • [7] 20, 12, pp. 91-97, (2020)
  • [8] 58, 8, pp. 1801-1810
  • [9] LIANG W, XIE S Y，, LONG J, A double PUF-based RFID identity authentication protocol in service-centric internet of things environments[J], Information Sciences, 503, pp. 129-147, (2019)
  • [10] 33, 12, pp. 1259-1262, (2013)
12