Formal Analysis Of Wireless Mesh Network Client Authencation Protocols Based On Event Logic

Security protocols ensure confidentiality,integrity and availability of resources in the process of interaction.Formal methods regulate security features of cryptographic protocols and have a more complete theoretical system and model.Theorem proving is a formal method to determine whether protocol satisfies security attributes to be validated under reasonable assumptions,based on rigorous mathematics theory knowledge and logical derivation.Event logic is a theorem proving method that describes state transitions and algorithms in concurrent and distributed systems and can be used to prove security of network protocols.Using event logic to analyze security of WMN client authentication protocol,reduce redundancy and complexity in protocol analysis and to improve efficiency of protocol analysis.the main work of this dissertation is as follows:(1)Combine event structures,axioms and random number lemma based on event logic,forward replacement rule to guarantee equivalent conversion of the protocol interactive user in equivalent substitution.Derive some properties to extend the application of event logic in protocol analysis such as multi-combination information interaction,non-overlapping,etc.(2)Describe basic sequence of interaction protocol between client and LTCA through event logic,and describe the protocol interactions formally.Prove strong authentication property of protocol,conclude authentication protocol between WMN client and LTCA are reasonable under assumption,and different entities can prove authentication by event logic.(3)Using event logic theory to prove security of authentication protocol between WMN clients after client user obtains the certificate issued by LCA.The result shows that WMN client authentication protocol is safe under reasonable assumption,which proves that event logic theory can not only prove the security attributes of wired network protocols but also prove the security attributes of wireless network protocols.This method guarantees reliability of security protocol during user interaction.(4)Describe event logic theory to prove the process of protocol security attributes.Simplify protocol formal verification steps through flow chart to reflect practicality of event logic theory.Compare and analyze event logic theory and other logical inference methods,show that event logic theory has generality.