华中科技大学学报（自然科学版）2024，Vol.52Issue(2)：69-76,8.DOI:10.13245/j.hust.240209
基于事件逻辑的PUFs认证协议形式化分析
Formal analysis of PUFs-based authentication protocols in logic of events theory
摘要
Abstract
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.关键词
形式化方法/事件逻辑(LoET)/物理不可克隆函数(PUFs)/双向认证协议/定理证明Key words
formal methods/logic of events theory(LoET)/physical unclonable functions(PUFs)/mutual authentication protocol/theorem proving分类
信息技术与安全科学引用本文复制引用
钟小妹,肖美华,杨科,罗运先..基于事件逻辑的PUFs认证协议形式化分析[J].华中科技大学学报（自然科学版）,2024,52(2):69-76,8.基金项目
国家自然科学基金资助项目(32260216,62362033,61962020) （32260216,62362033,61962020）
江西省教育厅科技项目(GJJ210623). （GJJ210623）
