Proving authentication property of PUF-based mutual authentication protocol based on logic of events

PUF (Physical unclonable function) is a new hardware security primitive, and the research on PUFs is one of the emerging research focuses. For PUF-based mutual authentication protocols, a method to abstract the security properties of hardware by using logic of events is proposed, and the application aspects of logic of events are extended to protocols based on hardware security. With the interaction of PUF-based mutual authentication protocol formally described by logic of events, the basic sequences are constructed and the strong authentication property in protocol interaction process is verified. Based on the logic of events, the freshness of nonces is defined, and the persist rule is proposed according to the concept of freshness, which ensures the consistency of the protocol state and behavior predicate in the proof process, and reduces the complexity and redundancy in the protocol analysis process. Under reasonable assumptions, the security of the protocol is proven, and the fact that logic of events applies to PUF-based mutual authentication protocols is shown.