Formal Analysis Of PUF-related Protocols Based On LoET-E

The key to ensure the security of communication system not only depends on the strength of the cryptographic algorithm used in the system,but also is closely related to the cryptographic protocols used.In some complex distributed networks,if the cryptographic protocols can not foresee all possible attacks in advance,it is easy to create huge potential safety hazards.The formal methods is one of the most powerful methods to prove the security of cryptographic protocols.Logic of events belongs to theorem proving,which is a kind of formal methods.Logic of events is designed based on message automata and defines all possible protocol actions.It provides new proof rules and mechanisms for protocol operation by assigning different types of keys,challenges and messages to protocol interactions.In this paper,the PUF-based mutual authentication protocol is analyzed based on the logic of events,an improved theory Lo ET-E is proposed by extending the axiomatic system and lemma of the logic of events,and the security attribute of the protocol is verified by using Lo ET-E,so that the logic of events is applicable to the emerging protocols.The main research results are as follows.1.Standardize the basic modeling theory in logic of events,including the relationship between Event-Orderings,Event Class and Event Structure,describe the challenges and its basic properties in detail,analyze the axiom system of logic of events,and improve the seven basic action classes and protocol formalization.2.Based on the logic of events,an improved theory Lo ET-E is proposed to prove the security properties of the protocols.It extends the definition of has in the flow relation axiom and the honesty axiom of existing logic of events,redefines the source of the acceptable signature of the honest principals,and improves the possible situation in the process of protocols' occurrence;introduces the concept Fresh and two derived concepts Gen and First Send,according to these three new concepts,a series of important rules are proposed.3.Three new concepts Safe,Safe Send and Safe Net are introduced on the basis of Lo ET-E,and a series of rules and corollaries are proposed according to these three concepts,which constitute a confidentiality proof system that can be used to prove confidentiality,and the provable security attribute of Lo ET-E is extended to confidentiality.4.Using Lo ET-E to analyze the security of the PUF-based mutual authentication protocol.According to the principle of PUF security implementation,it is the first time to use Lo ET-E to abstract function of PUF,define and sort the mutual authentication process of the protocol using the basic sequence,describe the security attributes of the mutual authentication protocol,and finally use the axiomatic system of Lo ET-E to verify its strong authentication attributes.It is concluded that the PUF-based mutual authentication protocol is safe under reasonable assumptions,which shows that Lo ET-E can be used to prove the authentication of different principals in the mutual authentication.