基于事件逻辑的PUFs认证协议形式化分析OA北大核心CSTPCD

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.