摘要
提出两个事件时序概念与相关规则,用于分析事件关联消息类型为挑战数的时态性质,形式化抽象物理不可克隆函数(PUFs)随机会话秘钥生成功能,扩展事件逻辑(LoET)用于形式化分析PUFs安全协议的理论.以一个基于SRAM PUFs(基于静态随机存取存储器的PUF类型)的安全双向认证协议分析为例,形式化规约了协议基于PUFs随机秘钥生成和双向认证过程,基于扩展的事件逻辑,采用定理证明方法推理证明了该协议在合理假设下满足双向强认证性质.研究表明扩展的事件逻辑理论可用于设计和分析基于PUFs安全协议.
ed 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 PUFsbased security protocols.
作者
钟小妹
肖美华
杨科
罗运先
ZHONG Xiaomei;XIAO Meihua;YANG Ke;Luo Yunxian(School of Software,East China Jiaotong University,Nanchang 330013,China)
出处
《华中科技大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2024年第2期69-76,共8页
Journal of Huazhong University of Science and Technology(Natural Science Edition)
基金
国家自然科学基金资助项目(32260216,62362033,61962020)
江西省教育厅科技项目(GJJ210623).
